General correctness: A unification of partial and total correctness
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.
- Unifying Recursion in Partial, Total and General Correctness
- Partial, total and general correctness
- Formalising general correctness
- Total correctness in nonstandard logics of programs
- General correctness algebra
- scientific article; zbMATH DE number 1531378
- An elementary and unified approach to program correctness
- Junctive compositions of specifications in total and general correctness
- Partial correctness: The term-wise approach
- Some general incompleteness results for partial correctness logics
- A characterization of weakest preconditions
- A logic covering undefinedness in program proofs
- A Powerdomain Construction
- A simple relation between relational and predicate transformer semantics for nondeterministic programs
- Consistent and complementary formal theories of the semantics of programming languages
- General correctness: A unification of partial and total correctness
- scientific article; zbMATH DE number 3662551 (Why is no real title available?)
- scientific article; zbMATH DE number 3740740 (Why is no real title available?)
- scientific article; zbMATH DE number 3757681 (Why is no real title available?)
- scientific article; zbMATH DE number 3532506 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- Nondeterministic Algorithms
- On the total correctness of nondeterministic programs
- Predicative programming Part I
- Some Properties of Predicate Transformers
- Predicate-transformer semantics of general recursion
- A calculus of refinements for program derivations
- Combining angels, demons and miracles in program specifications
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
- Specifications, programs, and total correctness
- Predicate transformers as power operations
- Towards reasoning about Hoare relations
- General correctness: A unification of partial and total correctness
- Infinite executions of lazy and strict computations
- Abstract commands: A uniform notation for specification and implementation
- Junctive compositions of specifications in total and general correctness
- Formalising general correctness
- Unifying correctness statements
- Of wlp and CSP
- Unifying Recursion in Partial, Total and General Correctness
- Relational mathematics for relative correctness
- Partial, total and general correctness
- Unifying theories of programming that distinguish nontermination and abort
- Reasoning about loops in total and general correctness
- Lifting General Correctness into Partial Correctness is ok
- General correctness algebra
- scientific article; zbMATH DE number 3902002 (Why is no real title available?)
- scientific article; zbMATH DE number 3921953 (Why is no real title available?)
- Multirelations with infinite computations
- scientific article; zbMATH DE number 2052653 (Why is no real title available?)
- scientific article; zbMATH DE number 1531378 (Why is no real title available?)
- Correctness of the formal generalized net project of the connections between procedural program functions
- An Inductive Theorem on the Correctness of General Recursive Programs
- Fixpoints for general correctness
- Partial correctness for probabilistic demonic programs
- Unifying wp and wlp
- Hoare logic for an imperative language considering some hardware limitations
- Algebras for iteration and infinite computations
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
- Partial correctness: The term-wise approach
- Dual unbounded nondeterminacy, recursion, and fixpoints
This page was built for publication: General correctness: A unification of partial and total correctness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265798)
