Auxiliary variables in data refinement

DOI10.1016/0020-0190(88)90227-XzbMath0662.68014OpenAlexW2003967246MaRDI QIDQ1114384

Carroll Morgan

Publication date: 1988

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

Full work available at URL: https://doi.org/10.1016/0020-0190(88)90227-x

zbMATH Keywords

program transformationdata refinementweakest preconditionprogramming methodology

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

Safety-critical Java programs from \textsf{Circus} models ⋮ Data refinement of predicate transformers ⋮ Algebraic proofs of consistency and completeness ⋮ A single complete rule for data refinement ⋮ Auxiliary variables in partial correctness programming logics

Cites Work

• Data refinement by calculation
• Laws of data refinement
• Data refinement of predicate transformers
• Proof of correctness of data representations
• Programming as a Discipline of Mathematical Nature
• Unnamed Item
• Unnamed Item