Logical animation
M. C. Costa, Ryan J. Cunningham, Joe Booth · 1990
When a formal specification of requirements is presented as a logical theory, symbolic animation of the theory can assist with validation. An animator displays a logical model of the formal specification. The authors show how minimal models can be derived from a tableau proof system. Examples illustrate the use of animation with a simple database and its use for validating specifications in the Modal Action Logic of the UK Alvey Forest Project. >