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

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

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item