Prespecification in data refinement

DOI10.1016/0020-0190(87)90224-9zbMath0624.68027OpenAlexW2152198540MaRDI QIDQ578901

Jifeng He, C. A. R. Hoare, 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)

Related Items (23)

Peirce algebras ⋮ An analysis of refinement in an abortive paradigm ⋮ Relational separation logic ⋮ Incompleteness of relational simulations in the blocking paradigm ⋮ Information flow in systems with schedulers. II: Refinement ⋮ Abstraction for concurrent objects ⋮ Jifeng He at Oxford and beyond: an appreciation ⋮ A pragmatic approach to stateful partial order reduction ⋮ Temporal-logic property preservation under Z refinement ⋮ A reification calculus for model-oriented software specification ⋮ The projection of systolic programs ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ Relational Concurrent Refinement: Automata ⋮ Data Refinement with Probability in Mind ⋮ Data refinement of predicate transformers ⋮ More Relational Concurrent Refinement: Traces and Partial Relations ⋮ A single complete rule for data refinement ⋮ Refinement and state machine abstraction ⋮ Relational Decomposition ⋮ Mechanizing some advanced refinement concepts ⋮ Parallel composition and decomposition of specifications ⋮ Normal form approach to compiler design ⋮ The lattice of data refinement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Non-deterministic data types: Models and implementations
• The weakest prespecification
• A calculus of communicating systems
• Proof of correctness of data representations
• Programming as a Discipline of Mathematical Nature

This page was built for publication: Prespecification in data refinement