Software Evolution with Refinement and Retrenchment

Given a record of the derivation of a component from its specification, and a new, changed specification, we can compare the two specifications and use the differences between them as a basis for revising the derivation of the component and attempt to discharge the resulting proof obligations. This is essentially the way that program refinements are modified by hand, and could be supported by a refinement tool. Alternatively, we might describe the new specification by combining the original specification and a description of the new behaviour required using combinators similar to schema conjunction and disjunction in Z. This approach has been explored in the context of the refinement calculus, and also in a relational setting. Independently of this revision-based and constructive work, another potential formal approach to the evolution of specifications has recently emerged. Retrenchment is a generalisation of classical refinement which was proposed to extend the reach of formal verification to applications too demanding to be described, computationally, in terms of refinement. Recent work has proposed the integration of these constructive and retrenchment approaches. This paper reports on initial work investigating the construction of evolutions using these constructive and retrenchment approaches. In special cases the evolution transformation may be a refinement. More widely applicable will be certain specification combinators and constructors. Finally, as the most general relation between specifications, retrenchment will be applicable to any evolution; the work will be in establishing how to use it to preserve structure in a useful way