The replay of program derivations

A promising though radical approach to software development is to write formal specifications and then derive implementations by applying sequences of formal steps. This is often known as transformational implementation. An advantage of this approach is increased consistency between specifications and implementations. But perhaps a more important advantage is the potential for maintaining specifications rather than implementations. Because derivation sequences formally describe how implementations are constructed, the user can modify specifications and then replay the derivations to obtain new implementations.This thesis discusses replaying derivations in an interactive environment. We identify several problems which need to be addressed to make replay both autonomous and robust. We present our implemented replay system, ReFocus, and describe how it addresses these problems. In particular, we present methods for updating derivations to match new specifications and for verifying the acceptability of implementations produced by replay.Updating derivations represents the technical core of this thesis. The system constructs analogical maps between specifications and applies them to derivations to solve new problems. Traditionally, analogical maps are constructed using first-order generalization, or anti-unification. However, we show that first-order generalization is too inflexible for program derivations. In its place, we propose using second-order generalization. We give a definition of second-order generalization, identify classes of terms for which such generalizations exist, and show that it is computable. We then identify an important subset of generalizations and give (under assumptions) a quadratic-time algorithm for computing this subset. Finally, we show that these generalizations provide the necessary flexibility for replay.We give a number of examples illustrating the usefulness of replay on small to medium-sized problems. For each, we show that ReFocus is able to obtain useful results. This demonstrates that replaying program derivations is both feasible and useful.U of I OnlyETDs are only available to UIUC Users without author permissio