Designing systems for future maintainability: A case study

A novel method is described for perfective maintenance of software which has been developed from specifications using formal transformations. The list of applied transformations provides a suitable derivation history to use when changes are made to the software. A comparison is made between sequential transformations and standard proof-based refinement techniques for providing this derivation history, based upon the case study of a library system. When using criteria such as scaleability, speed, ease, design improvements and software quality, transformations are a more favorable basis of refinement. The method produces software which is well structured and highly maintainable