General correctness: A unification of partial and total correctness

DOI10.1007/BF00290146zbMath0559.68021OpenAlexW1990589200MaRDI QIDQ2265798

David Gries, Dean Jacobs

Publication date: 1985

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00290146

zbMATH Keywords

semanticsnondeterminismpredicate transformersweakest preconditionGeneral correctnesspartial and total correctnessweakest and strongest postconditions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Predicate transformers as power operations, A calculus of refinements for program derivations, Towards reasoning about Hoare relations, Multirelations with infinite computations, Of wlp and CSP, Combining angels, demons and miracles in program specifications, Fixpoints for general correctness, General correctness: A unification of partial and total correctness, Algebras for iteration and infinite computations, Dual unbounded nondeterminacy, recursion, and fixpoints, Infinite executions of lazy and strict computations, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic covering undefinedness in program proofs
• On the total correctness of nondeterministic programs
• A simple relation between relational and predicate transformer semantics for nondeterministic programs
• A characterization of weakest preconditions
• General correctness: A unification of partial and total correctness
• Consistent and complementary formal theories of the semantics of programming languages
• Predicative programming Part I
• A Powerdomain Construction
• Some Properties of Predicate Transformers
• Nondeterministic Algorithms