Author: Lindsay Groves
Source: GZipped PostScript (55kb); Adobe PDF
(297kb)
Formal program derivations are difficult to understand because of the amount of detail that needs to be presented. We discuss a way of presenting program derivations in the refinement calculus, based on a form of structure diagram, annotated with formal specifications and details of refinement steps. We also show that these diagrams can be used as a basis for constructing formal derivations for existing programs.