Analyzing and Animating Declarative Specifications.
Stelvio Cimato, Cecilia Mascolo · 1996
Z is a declarative, not executable specification language. We introduce two methods for formal analysis and testing of behavioral aspects of Z specifications. We define a chemical operational semantics, which supports an abstract execution model and some new logic constructs to allow the verification of dynamic properties. We then describe a parallel animator of Z specifications which automatically constructs distributed prototypes in Shared Prolog directly from a refined specification. 1 Introduction The introduction of formal methods in software engineering practice can increase the quality and the reliability in the development process of complex software systems. Specification documents, written with mathematical notation, give a more precise and rigorous description of the system being developed, reducing possible ambiguities and inconsistencies. Consequently, errors can be earlier recognized and earlier corrected, saving in this way time and money. Z notation is a well k...