Files in this item



application/pdf9522116.pdf (8MB)Restricted to U of Illinois
(no description provided)PDF


Title:The replay of program derivations
Author(s):Hasker, Robert W.
Doctoral Committee Chair(s):Reddy, Uday S.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
Abstract: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.
Issue Date:1995
Rights Information:Copyright 1995 Hasker, Robert W.
Date Available in IDEALS:2011-05-07
Identifier in Online Catalog:AAI9522116
OCLC Identifier:(UMI)AAI9522116

This item appears in the following Collection(s)

Item Statistics