Auxiliary variables in data refinement

DOI10.1016/0020-0190(88)90227-XMaRDI QIDQ1114384zbMATH OpenOpenAlexFDO

Authors 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

weakest preconditionprogram transformationdata refinementprogramming methodology

Mathematics Subject Classification ID

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

Recommendations

• Effectively eliminating auxiliaries
• Some proofs of data refinement
• The role of auxiliary variables in the formal development of concurrent programs
• Data refinement by calculation
• A single complete rule for data refinement

Cites work

• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• Data refinement by calculation
• Data refinement of predicate transformers
• Laws of data refinement
• Programming as a Discipline of Mathematical Nature
• Proof of correctness of data representations

Cited in

(7)

• Auxiliary variables in partial correctness programming logics
• The role of auxiliary variables in the formal development of concurrent programs
• Effectively eliminating auxiliaries
• Data refinement of predicate transformers
• Safety-critical Java programs from \textsf{Circus} models
• A single complete rule for data refinement
• Algebraic proofs of consistency and completeness

This page was built for publication: Auxiliary variables in data refinement

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