Executing diagram sequences

Abstract

We present a general framework for using diagram sequences as plan specifications. We also present an implemented system based on that framework, which generates imperative programs from diagram sequences similar to those used in teaching programming. The specific notations we use in the system are based closely on the diagrams typically used for teaching introductory programming, but the framework is general enough to account for and express many uses of diagram sequences. The system and the underlying theory highlight some areas where planning, reasoning about action, the refinement calculus and diagrammatic reasoning are synergistic. For example, by framing the definition of algorithms as a type of plan specification, it becomes clear that decomposition of a planning problem into sub-plans is analogous to refinement in the software engineering sense. More importantly, the system gives insight into the underlying structure of the largely informal use of diagrams that is routinely found in the explanation of algorithms. Obvious applications include teaching (since the inspiration for the system is a common method for teaching) and software engineering, where diagrams are often used to specify type systems rigorously (e.g. class diagrams), but specify program dynamics informally.