Author: Lindsay Groves
Source: GZipped PostScript (52kb); Adobe PDF
(285kb)
We present an approach to formal program derivation integrating ideas from the refinement calculus with structure diagrams, and discuss how it might be supported by a refinement tool. This approach allows program derivations to be presented, and constructed, in a diagrammatic formalism which is similar to traditional structure diagrams but has well-defined semantics. The approach allows formal and informal derivation to be combined, and allows formal derivations to be constructed in more flexible ways than existing refinement tools.