The weakest prespecification

DOI10.1016/0020-0190(87)90106-2MaRDI QIDQ1091121zbMATH OpenOpenAlexFDO

Authors Jifeng He, Tony Hoare

Publication date 1987

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(87)90106-2

zbMATH Keywords

general recursionguarded commandrelational calculusweakest preconditionweakest prespecification

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3974258
• Proof system for weakest prespecification
• scientific article; zbMATH DE number 4020448
• scientific article; zbMATH DE number 4068837
• A Weakest Precondition Semantics for Z

Cites work

• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 3660783 (Why is no real title available?)
• The mathematical construction of a program

Cited in

(36)

• Proof system for weakest prespecification
• Inductive data types for predicate transformers
• A representation theorem for quantales
• Normal form approach to compiler design
• Peirce algebras
• Towards automating duality
• Semantic distance between specifications
• The logic of Peirce algebras
• Relations and non-commutative linear logic
• Towards reasoning about Hoare relations
• A relational division operator: The conjugate kernel
• The weakest specifunction
• Gentzen-type calculi for involutive quantales
• Automated reasoning for probabilistic sequential programs with theorem proving
• Unambiguous Büchi Is Weak
• A relation-algebraic approach to multirelations and predicate transformers
• Relational decomposition
• scientific article; zbMATH DE number 3974258 (Why is no real title available?)
• scientific article; zbMATH DE number 4020448 (Why is no real title available?)
• scientific article; zbMATH DE number 4068837 (Why is no real title available?)
• A Weakest Precondition Semantics for Z
• scientific article; zbMATH DE number 8784 (Why is no real title available?)
• A relation-algebraic approach to the ``Hoare logic of functional dependencies
• Quantales, observational logic and process semantics
• Autonomous posets and quantales
• Prespecification in data refinement
• An elementary and unified approach to program correctness
• Jifeng He at Oxford and beyond: an appreciation
• Formally verified animation for RoboChart using interaction trees
• Assume-guarantee reasoning for additive hybrid behaviour
• Representation theorems for \(Q\)-algebras
• Embedding a demonic semilattice in a relation algebra
• Constructor theory as process theory
• Free quantaloids
• Angelic nondeterminism in the unifying theories of programming
• Process simulation and refinement

This page was built for publication: The weakest prespecification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1091121)