Prototyping Z specifications in extended Lisp.

Much research has identified shortcomings in the Requirements Description to be the key factor in the failure of many software development projects; the development of formal specification techniques and notations allows the unambiguous statement of requirements, against which an implementation can generally be verified or even proved. While this approach will resolve many of the difficulties, it is impossible to formally confirm that such a specification is correct with respect to the intention of the customer; the abstraction that is characteristic of such languages can make the formal specification inaccessible without specialist skills. Z is one such, model-based, specification notation and this thesis reports on a CASE tool, the Z Animator in Lisp, that supports a process of specification validation through animation. A specification in the proprietary ZAL format, a high-level, largely functional, executable notation based on extended Lisp, can be executed by the Animation Engine within the ZAL animation environment. Using a graphical environment running under Microsoft Windows, schemas representing the operations upon the state are animated by populating their inputs, evaluating their predicates and reporting the outcomes to the user; these outcomes can be used to directly update the state, prior to further executions. The animator ensures the consistency of the on-going model state by the execution of the system invariant. The user can identify precisely which elements of the state should be displayed and can thereby focus on the particular areas of interest. This interaction is significantly more accessible to the customer and can be used to explore properties of the specification and thereby confirm, or not, that it exhibits the desired behaviour. This process validates the specification with respect to customer intention.Because the transformation into the proprietary ZAL language can be largely automated, using a companion CASE tool called TranZit, the process supports theiterative development of an improved specification, since at each stage the Z document reflects the system being animated.