Show simple item record

dc.contributor.authorJacobs, Deanen_US
dc.contributor.authorGries, Daviden_US
dc.description.abstractGeneral 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.en_US
dc.format.extent1444637 bytes
dc.format.extent437790 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleGeneral Correctness: A Unification of Partial and Total Correctnessen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record