Generating Program Animators from Programming Language Semantics

Dave Berry

Abstract: I present a theory of program animation based on formal semantics. This theory shows how an animator for a language can be generated from a formal specification of that language. Such an animator presents a model of evaluation that is formally correct with respect to the semantics. The theory also provides a framework for comparing definitions of animation operations.

The main part of the theory is the definition of an evaluation step. I compare two definitions. The first is based on the transitions used in the transitional style of structured operational semantics, and is motivated by the idea that these transitions represent an intuitive idea of a computation step. Unfortunately this definition produces unsatisfactory animations. However, it can be augmented to give one that better satisfies the needs of the user.

Both of these definitions are given in the relational style of structured operational semantics. The first definition is based on an equivalence between the relational and transitional styles; I give a definition of this equivalence. I also discuss the relation between the definition of a step and the choice of semantic formalism.

Views of a program in mid-evaluation can be defined by extending the specification of the programming language to include semantic display rules. Each semantic display rule specifies the display of one sub-phrase of the program in mid-evaluation. This approach is powerful enough to define a wide range of views. I also show how the definition of a step can be parameterised on a view.

More advanced operations can also be defined in terms of this theory. These operations and the views mentioned in the previous paragraph cover most of the features found in existing animators. This indicates that the theory is powerful enough to specify useful systems. The main feature that is not yet provided is the ability to define views that are specific to a single program.

These ideas have been implemented in a system called the Animator Generator. Animators produced by The Animator Generator support multiple views and the advanced operations mentioned here. I give a brief description of this system. I finish by discussing how this work could be developed further.

PhD Thesis - Price £10.00

LFCS report ECS-LFCS-91-163 (also published as CST-79-91)

Previous | Index | Next