Program Comprehension with the Refinement Calculus


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.

[Up to Computer Science Technical Report Archive: Home Page]