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

data refinementprogram transformationprogramming methodologyweakest precondition

Mathematics Subject Classification ID

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

Review text

A set of local variables in a program is auxiliary if its members occur only in assignments to members of the same set. Data refinement transforms a program, replacing one set of local variables by another set, in order to move towards a more efficient representation of data. Most techniques of data refinement give a direct transformation. But there is an indirect technique, using auxiliary variables, that proceeds in several stages. Usually, the two techniques are considered separately. It is shown that the several stages of the indirect technique are themselves special cases of the direct one, thus unifying the separate approaches. Removal of auxiliary variables is formalized incidentally.

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

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

Cited in

(7)

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

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)