Prespecification in data refinement

DOI10.1016/0020-0190(87)90224-9MaRDI QIDQ578901zbMATHOpenAlexFDO

Authors Tony Hoare, Jifeng He, Jeff W. Sanders

Publication date 1987

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(87)90224-9

zbMATH Keywords

data refinementabstract data typeconcrete data typenondeterministic procedural programming languagepostspecificationprespecificationweakest specification

Mathematics Subject Classification ID

Data structures (68P05)

Recommendations

• scientific article; zbMATH DE number 3943003
• Laws of data refinement
• Data refinement by calculation
• A single complete refinement rule for Z
• Some proofs of data refinement

Cites work

• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 3660783 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• A calculus of communicating systems
• Non-deterministic data types: Models and implementations
• Programming as a Discipline of Mathematical Nature
• Proof of correctness of data representations
• The weakest prespecification

Cited in

(30)

• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 827943 (Why is no real title available?)
• A pragmatic approach to stateful partial order reduction
• The lattice of data refinement
• Formal communication elimination and sequentialization equivalence proofs for distributed system models
• Mechanizing some advanced refinement concepts
• A single complete refinement rule for Z
• Peirce algebras
• Relational concurrent refinement: automata
• A reification calculus for model-oriented software specification
• An analysis of refinement in an abortive paradigm
• Data refinement with probability in mind
• Abstraction for concurrent objects
• Normal form approach to compiler design
• Parallel composition and decomposition of specifications
• Temporal-logic property preservation under Z refinement
• The projection of systolic programs
• Information flow in systems with schedulers. II: Refinement
• Data refinement of predicate transformers
• More relational concurrent refinement: traces and partial relations
• Incompleteness of relational simulations in the blocking paradigm
• Assume-guarantee reasoning for additive hybrid behaviour
• A single complete rule for data refinement
• Correct Hardware Design and Verification Methods
• Data refinement by calculation
• Refinement and state machine abstraction
• Composition and refinement of specifications of parameterized data types
• Relational decomposition
• Relational separation logic
• Jifeng He at Oxford and beyond: an appreciation

This page was built for publication: Prespecification in data refinement

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