A single complete rule for data refinement

DOI10.1007/BF01212407zbMATH Open0774.68081OpenAlexW4241804335MaRDI QIDQ684396FDOQ684396

Authors 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

completenessprogram verificationrefinement calculusweakest preconditionabstract datatypesbounded nondeterminismlanguage constructsspecification techniques

Mathematics Subject Classification ID

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

Recommendations

• A single complete refinement rule for Z
• scientific article; zbMATH DE number 3943003
• Some proofs of data refinement
• Laws of data refinement
• A Practical Single Refinement Method for B

Cites work

• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• A single complete rule for data refinement
• Auxiliary variables in data refinement
• Data refinement by calculation
• Data refinement of predicate transformers
• Laws of data refinement
• Prespecification in data refinement
• Proof of correctness of data representations
• The existence of refinement mappings
• The specification statement

Cited in

(24)

• The lattice of data refinement
• A single complete refinement rule for Z
• Programming interfaces and basic topology
• Unification: A case-study in data refinement
• A Practical Single Refinement Method for B
• A formal software development approach using refinement calculus
• Power simulation and its relation to traces and failures refinement
• An analysis of refinement in an abortive paradigm
• Algebraic proofs of consistency and completeness
• Data refinement with probability in mind
• Soundness of data refinement for a higher-order imperative language
• Laws of data refinement
• Temporal-logic property preservation under Z refinement
• Information flow in systems with schedulers. II: Refinement
• Blaming the client: on data refinement in the presence of pointers
• A single complete relational rule for coalgebraic refinement
• A single complete rule for data refinement
• On the antisymmetry of Galois embeddings
• scientific article; zbMATH DE number 1759495 (Why is no real title available?)
• Auxiliary variables in data refinement
• Data refinement and singleton failures refinement are not equivalent
• Refinement and state machine abstraction
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Relational separation logic

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

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