A Logic for Correct Program Development

Abstract

Existing verification technology, though theoretically adequate, is not directly applicable to the construction of large software systems. This thesis explores the view that reasoning about code is not the proper paradigm for correct program development. Instead, specifications should be the objects of study and a logic should be formulated for constructively proving that specifications have acceptable implementations; from these proofs code may be extracted. Thus, constructive existence proofs become the programmer's main concern, while executable text is seen as a valuable by-product of correct reasoning which cannot be produced from incorrect reasoning. The thesis captures this view of program development in a logic for the formal refinement of specifications. Specifications are written in an imperative notation of generalized assignment; they allow calculations in integer arithmetic and finite set theory. Classical reasoning techniques are shown inconsistent in this domain (where propositions may claim the constructive existence of programs), hence an alternative logic is developed based on intuitionistic reasoning. Proofs in this constructive refinement logic are trees, stylistically similar to those of Gerhard Gentzen's sequent calculus. It is argued that while linear proofs are appropriate when reasoning is developed and presented on paper, hierarchical proofs are appropriate when reasoning is developed and presented with machine aid. A mechanism is described that extracts correct codes from valid proofs; its existence assures the consistency of the logic. Finally, several code optimization techniques are examined and applied to code extracted from sample proofs. The thesis concludes with a discussion of the expounded view of correct program development, suggestions for a program development system based on this view, and a look at the numerous research problems remaining in this area.