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/6480
Title: General Correctness: A Unification of Partial and Total Correctness
Authors: Jacobs, Dean
Gries, David
Keywords: computer science
technical report
Issue Date: Oct-1984
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-641
Abstract: General correctness, which subsumes partial and total correctness, is defined for both weakest preconditions and strongest postconditions. Healthiness properties for general-correctness predicate transformers are more uniform and complete than those for partial-and-total-correctness systems. In fact, the healthiness properties for partial and total correctness are simple restrictions of those for general correctness. General correctness allows simple formulations of the connections between weakest and strongest postconditions and between the notions of weakest precondition under the "demonic" and "angelic" interpretations of nondeterminism. A problem that plagues $sp - sp(P, C)$ is undefined if execution of $C$ begun in some state of $P$ may not terminate - disappears with the generalization. This paper is a study of some simple theory underlying predicate transformer semantics, and as yet has little bearing on current programming practices. The theory uses a relational model of programs.
URI: http://hdl.handle.net/1813/6480
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
84-641.pdf1.41 MBAdobe PDFView/Open
84-641.ps427.53 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us