A single complete rule for data refinement
DOI10.1007/BF01212407zbMATH Open0774.68081OpenAlexW4241804335MaRDI QIDQ684396FDOQ684396
Paul H. B. Gardiner, Carroll Morgan
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
Recommendations
completenessprogram verificationrefinement calculusweakest preconditionabstract datatypesbounded nondeterminismlanguage constructsspecification techniques
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- The existence of refinement mappings
- Proof of correctness of data representations
- Title not available (Why is that?)
- The specification statement
- Prespecification in data refinement
- A single complete rule for data refinement
- Title not available (Why is that?)
- Title not available (Why is that?)
- Data refinement by calculation
- Auxiliary variables in data refinement
- Data refinement of predicate transformers
- Laws of data refinement
Cited In (23)
- Unification: A case-study in data refinement
- A Single Complete Relational Rule for Coalgebraic Refinement
- On the antisymmetry of Galois embeddings
- Laws of data refinement
- Data Refinement with Probability in Mind
- Soundness of data refinement for a higher-order imperative language
- Refinement and state machine abstraction
- Auxiliary variables in data refinement
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Power simulation and its relation to traces and failures refinement
- An analysis of refinement in an abortive paradigm
- Data refinement and singleton failures refinement are not equivalent
- A formal software development approach using refinement calculus
- A Practical Single Refinement Method for B
- Relational separation logic
- Programming interfaces and basic topology
- Title not available (Why is that?)
- The lattice of data refinement
- Information flow in systems with schedulers. II: Refinement
- Temporal-logic property preservation under Z refinement
- A single complete rule for data refinement
- A single complete refinement rule for Z
- Algebraic proofs of consistency and completeness
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)
