Data refinement of predicate transformers

DOI10.1016/0304-3975(91)90029-2zbMath0736.68060OpenAlexW2073708948MaRDI QIDQ1177155

Carroll Morgan, Paul H. B. Gardiner

Publication date: 26 June 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(91)90029-2

zbMATH Keywords

specificationdata refinementpredicate transformersguarded commands

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items (17)

Angelic nondeterminism in the unifying theories of programming ⋮ Data refinement, call by value and higher order programs ⋮ Auxiliary variables in data refinement ⋮ Blaming the client: on data refinement in the presence of pointers ⋮ External and internal choice with event groups in Event-B ⋮ Refinement concepts formalised in higher order logic ⋮ Algebraic proofs of consistency and completeness ⋮ Games and winning strategies ⋮ A single complete rule for data refinement ⋮ A Generalisation of Stationary Distributions, and Probabilistic Program Algebra ⋮ Angelic processes for CSP via the UTP ⋮ A formal software development approach using refinement calculus ⋮ Set-Theoretic Models of Computations ⋮ Mechanizing some advanced refinement concepts ⋮ A formal model of real-time program compilation ⋮ Soundness of data refinement for a higher-order imperative language ⋮ The lattice of data refinement

Cites Work

• A theoretical basis for stepwise refinement and the programming calculus
• Prespecification in data refinement
• Laws of data refinement
• Auxiliary variables in data refinement
• Proof of correctness of data representations
• Specification statements and refinement
• A Weaker Precondition for Loops
• The specification statement
• Programming as a Discipline of Mathematical Nature
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Data refinement of predicate transformers