Search

We show how machine-checked verification can support an approach to circuit design based on transformations. This approach starts with a conceptually simple (but inefficient) initial design and uses a combination of ad hoc and algorithmic transformations to produce a design that is more efficient (but more complex).

The checkability designed into the LSL (Larch shared language) is described, and two tools that help perform the checking are discussed. LP (the Larch power) is the principal debugging tool. Its design and development have been motivated primarily by work on LSL, but it also has other uses (e.g. reasoning about circuits and concurrent algorithms). Because of these other uses, and because they also tend to use LP to analyze Larch interface specifications, the authors have tried not to make LP too LSL-specific. Instead, they have chosen to build a second tool, LSLC (the LSL checker), to serve as a front-end to LP. LSLC checks the syntax and static semantics of LSL specifications and generates LP proof obligations from their claims. These proof obligations fall into three categories: consistency (that a specification does not contradict itself), theory containment (that a specification has intended consequences), and relative completeness (that a set of operators is adequately defined). An extended example illustrating how LP is used to debug LSL specifications is presented. >

The programming language Euclid has been designed to facilitate the construction of verifiable system programs. By a verifiable program we mean one written in such a way that existing formal techniques for proving certain properties of programs can be readily applied; the proofs might be either manual or automatic, and we believe that similar considerations apply in both cases. By system we mean that the programs of interest are part of the basic software of the machine on which they run; such a program might be an operating system kernel, the core of a data base management system, or a compiler. An important consequence of this goal is that Euclid is not intended to be a general-purpose programming language. Furthermore, its design does not specifically address the problems of constructing very large programs; we believe most of the programs written in Euclid will be modest in size. While there is some experience suggesting that verifiability supports other desired goals, we assume the user is willing, if necessary, to obtain verifiability by giving up some run-time efficiency, and by tolerating some inconvenience in the writing of his programs.

Larch specifications are two-tiered. Each one has a component written in an algebraic language and another tailored to a programming language.

This handbook consists of a collection of traits written in the Larch Shared Language, and is intended as a companion to the “Report on the Larch Shared Language”. It should serve three distinct purposes: •- Provide a set of components that can be directly incorporated into other specifications;•- Provide a set of models upon which other specifications can be based; and•- Help people to better understand the Larch Shared Language by providing a set of illustrative examples.

These notes are personal reflections, stemming from attempts to understand the sources of problems and successes in the application of work on formal specifications. Our intent is to provoke thought about the nature and value of work in the area; not to provide a set of well-tested results. Rather than focusing on yet another specification language, we have tried to take a broad view of the role of formal specifications in the program development process.

The choice of programming language for a large systems software effort can have profound economic implications. A major point of disagreement is the level of language which should be chosen. This debate features representatives of both the academic and industrial communities, focusing on those issues where disagreement is strong.

It has frequently been remarked that it is easier recognize “high level” languages than to define the concept. For the purposes of this debate, however, I think that we agree that a language is high level to the extent that it discourages (forbids) the specification of machine details (register numbers, absolute addresses, op codes, word-packing, etc.) as a routine part of program composition and low level to the extent that it encourages (requires) such specification. (Note that, by this definition, assembly languages occupy a position intermediate between machine languages and compiled languages.) Thus, I take the point at issue to be: “To what extent is it desirable for the system programmer to specify machine details?”

In the spirit of the previous axiomatixation of the programming language Pascal, this paper describes Hoare-style proof rules for Euclid, a programming language intended for the expression of system programs which are to be verified. All constructs of Euclid are covered except for storage allocation and machine dependencies.