An approach to formal reasoning about programs

This thesis presents a formal apparatus which is adequate both to express the termination and correctness properties of programs and also the necessary induction rules and axioms of their domains. He explore the applications of this formalism with particular emphasis on providing a basis for formalising the stepwise-development of programs. The formalism provides, in some sense, the minimal extension into a second order theory that is required. It deals with binary relations between tuples and the minimal fixpoints of monotone and continuous functionals on them. The correspondence between common constructs in programming languages and this formalism is shown in an informal manner. To show correctness of a program it is necessary to find an expression for its termination properties which will depend on the induction rules for the data structures of the program. We show how these rules may be formally expressed and manipulated to derive other induction rules, and give a technique for mechanically deriving from a schema an expression for its domain which may be expressed in terms of given induction rules by the manipulations referred to above. We give axiomatic definitions, including an induction rule, for some domains, which commonly occur in programs, these being finite sets, trees, structures, arrays with fixed bounds, LISP S-expressions, linear lists, and the integers. In developing a program one may start by defining the basic operations and domains in an axiomatic manner. Development proceeds by finding satisfactory representations for this domain in terms of more specific domains and their operations, until finally one has domains which are representable in a target language. We discuss what is meant by a representation in an attempt to formalise this technique of data refinement, and also mention the less general notion of simulation which requires that a representation is adequate tor a particular program to work. A program may have been developed in a recursive manner and if the target language does not contain recursion as a basic primitive it will be necessary to simulate it using stacks. We give axioms for such stacks, and give a mechanical procedure for obtaining from any recursive program, a flowchart program augmented by stacks, which simulates it