Author: Lindsay Groves
Source: GZipped PostScript (55kb); Adobe PDF
(300kb)
The refinement calculus is usually presented as a formalisation of stepwise refinement, so there is an (often tacit) assumption that programs are going to be constructed from scratch, in a strictly top-down fashion. Most of the rules in the refinement calculus are concerned with decomposing specifications into more procedural forms, and existing refinement tools primarily provide support for this kind of construction.We argue that in order to support more realistic styles of program construction, we need to consider ways in which an existing program derivation can be adapted to reflect a modification in the initial specification, or perhaps to produce a different algorithm for the same specification. This will allow us to support more flexible styles of program construction, such as incremental enhancement, and also to provide support for program maintenance.
We discuss some of the mechanisms required to support adaptation of formal derivations in the refinement calculus, and outline the architecture of a proposed tool to support this style style, based on the idea of an editable derivation script. We then show how this approach can be used to adapt formal derivations to obtain programs to satisfy different specifications.