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)

Review text

This paper introduces the concept of the weakest prespecification of program Q with respect to specification R, written \(Q\setminus R\), and explores its basic properties within the framework of the relational calculus. The weakest prespecification serves the same purpose as Dijkstra's weakest precondition, but generalises it in four ways. (1) The specification R describes not only the desired properties of the final values of the variables, but also their desired relationship with the initial values; such specifications are normal in specification languages like VDM and Z. (2) The program Q may be just the specification of a program still to be written. Consequently, the weakest prespecification can assist in splitting a task R into two subtasks Q and \(Q\setminus R\). (3) A partial relation R is taken as the specification of a guarded command, thus guarded commands can be specified and implemented independently, before being collected into a set with if or do. (4) The programming language is extended to include general recursion.

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

(37)

• 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
• ConcurrentHOL
• 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)