A Logic for Correct Program Development

Other Titles


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.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record