Symbolic Animation as a Proof Tool

This paper illustrates how animation conversions [14] which help in preliminary debugging of behavioural definitions, can subsequently be used as effective proof tools which play an important role in the verification of properties related to the definitions. We illustrate this point by specifying a simple compiler to map constructs of a toy imperative programming language into instructions which run on a rudimentary abstract machine. The same conversions used to symbolically compile programs of the language and to execute the resulting machine instructions are used in the verification of the compiler. This paper suggests that conversions provide a sound basis for a proof methodology with formal animation acting as an integral step in a verification process.