eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6295
Title:  A Logic for Correct Program Development 
Authors:  Bates, Joseph L. 
Keywords:  computer science technical report 
Issue Date:  Mar1981 
Publisher:  Cornell University 
Citation:  http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81455 
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 byproduct 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. 
URI:  http://hdl.handle.net/1813/6295 
Appears in Collections:  Computer Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
