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 (17)

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

This page was built for publication: A single complete rule for data refinement