Abstract
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.