A single complete rule for data refinement

DOI10.1007/BF01212407zbMath0774.68081OpenAlexW4241804335MaRDI QIDQ684396

Carroll Morgan, Paul H. B. Gardiner

Publication date: 15 September 1993

Published in: Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

completenessrefinement calculusprogram verificationweakest preconditionabstract datatypesbounded nondeterminismlanguage constructsspecification techniques

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items

Power simulation and its relation to traces and failures refinement, An analysis of refinement in an abortive paradigm, Relational separation logic, Information flow in systems with schedulers. II: Refinement, A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, Temporal-logic property preservation under Z refinement, A Practical Single Refinement Method for B, A Single Complete Relational Rule for Coalgebraic Refinement, Data Refinement with Probability in Mind, Algebraic proofs of consistency and completeness, A single complete rule for data refinement, A formal software development approach using refinement calculus, Refinement and state machine abstraction, Programming interfaces and basic topology, On the antisymmetry of Galois embeddings, Soundness of data refinement for a higher-order imperative language, The lattice of data refinement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Prespecification in data refinement
• A single complete rule for data refinement
• The existence of refinement mappings
• Data refinement by calculation
• Laws of data refinement
• Auxiliary variables in data refinement
• Data refinement of predicate transformers
• Proof of correctness of data representations
• The specification statement