Skip to main content


eCommons@Cornell

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: Mar-1981
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-455
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.
URI: http://hdl.handle.net/1813/6295
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
81-455.pdf5.43 MBAdobe PDFView/Open
81-455.ps1.93 MBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us