General correctness: A unification of partial and total correctness (Q2265798)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | General correctness: A unification of partial and total correctness |
scientific article |
Statements
General correctness: A unification of partial and total correctness (English)
0 references
1985
0 references
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.
0 references
General correctness
0 references
partial and total correctness
0 references
predicate transformers
0 references
weakest and strongest postconditions
0 references
weakest precondition
0 references
nondeterminism
0 references
semantics
0 references
0 references