Auxiliary variables in data refinement

DOI10.1016/0020-0190(88)90227-XzbMATH Open0662.68014OpenAlexW2003967246MaRDI QIDQ1114384FDOQ1114384

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

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

zbMATH Keywords

weakest preconditionprogram transformationdata refinementprogramming methodology

Mathematics Subject Classification ID

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

Cites Work

• Proof of correctness of data representations
• Title not available (Why is that?)
• Programming as a Discipline of Mathematical Nature
• Title not available (Why is that?)
• Data refinement by calculation
• Data refinement of predicate transformers
• Laws of data refinement

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)