The lattice of data refinement

DOI10.1007/BF01192157zbMath0790.68028OpenAlexW4239538615MaRDI QIDQ1323380

V. Pereyra

Publication date: 4 July 1994

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01192157

zbMATH Keywords

refinement calculusdata refinementprogram developmentangelic nondeterminismdemonic nondeterminismmicracles

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) General topics in the theory of software (68N01)

Related Items

External and internal choice with event groups in Event-B

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Prespecification in data refinement
• A single complete rule for data refinement
• Data refinement by calculation
• Duality in specification languages: A lattice-theoretical approach
• A calculus of refinements for program derivations
• Laws of data refinement
• Data refinement of predicate transformers
• Statement inversion and strongest postcondition
• Proof of correctness of data representations
• The specification statement