Abstract: 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.
Publication Year: 1994
Publication Date: 1994-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 5
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot