A framework is presented for adding a general Undo facility to programming languages. A discussion of relevant literature is provided to show that the idea of Undoing pervades several areas in computer science, and even other disciplines. A simple model of computation is introduced, and it is augmented with a minimal amount of additional structure needed for recovery and reversal. Two different interpretations of Undo are motivated with examples. Then, four primitives are defined in a language-independent manner; they are sufficient to support a wide range of Undo capability. Two of these primitives carry out state saving, and the others mirror the two versions of the Undo operation. Properties of and relationships between these primitives are explored, and there are some preliminary remarks on how one could implement a system based on this formalism. The main conclusion is that the notions of recovery and reversal of actions can become part of the programming process.

In this paper we describe how we have combined a number of tools (most of which understand a particular programming language) into a single system to aid in the reading, writing, and running of programs. We discuss the efficacy and the structure of our system. For the last two years the system has been used to build itself; it currently consists of 500 kilobytes of machine code (25,000 lines of LISP/370 code) and approximately one hundred commands with large numbers of options. We will describe some of the experience we have gained in evolving this system. We first indicate the system components which users have found most important; some of the tools described here are new in the literature. Second, we emphasize how these tools form a synergistic union, and we illustrate this point with a number of examples. Third, we illustrate the use of various system commands in the development of a simple program. Fourth, we discuss the implementation of the system components and indicate how some of them have been generalized.

A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman [1]. However, the computer discussed has some realistic characteristics not shared by the machine treated in [1], and the details of the microcode validation are complicated by this fact. A formal technique for partitioning the proof is presented and illustrated with examples.