Z specifications meet Mathematica for exploratory prototyping
Linda B. Sherrell, William H. Paulsen · 2002
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.