Z specifications meet Mathematica for exploratory prototyping

In order for formal methods to achieve widespread acceptance, associated tools must become more accessible to the average user. This work describes ZEM (Z Embedded in Mathematica), a new tool supporting the major phases of the requirements analysis life cycle. ZEM is best described as an animator for Z specifications with a theorem proving component. The overall goal in its design has been twofold: (1) to encourage the use of formal methods by a wider group of practitioners and (2) to provide an environment that facilitates exploratory prototyping.