Z/EVES

As of June 2005, ORA Canada can no longer distribute Z/EVES.

Z/EVES 2.4.1 was the last version released. This version includes a graphical user interface that allows Z specifications to be entered, edited, and analysed in their typeset form; supports the incremental analysis of specifications; and manages the synchronization of the analysis with modifications to the specification. Some screen shots are available.

Z/EVES uses state-of-the-art formal methods techniques from Europe and North America, integrating a leading specification notation with a leading automated deduction capability. The resulting system supports the analysis of Z specifications in several ways:

• syntax and type checking,
• schema expansion,
• precondition calculation,
• domain checking, and
• general theorem proving.

Users can be introduced to Z/EVES in steps. For example, little knowledge of the theorem prover is required for syntax and type checking, schema expansion, and precondition calculation. Even with domain checking, many of the proof obligations are easily proven. In more difficult cases, generating the proof obligation is often a substantial aid in determining whether a specification is meaningful.

Z/EVES supports almost the entire Z notation; only the unique existence quantifier for schema expressions is not yet supported. The Z/EVES prover provides powerful automated support (e.g., heuristics and conditional rewriting) with user commands for directing the prover (e.g., instantiate a specific variable or introduce a lemma). Z/EVES includes support for the Mathematical Toolkit as described in Spivey's 2nd edition of "The Z Notation."

Interaction with the Z/EVES system uses either the GUI described above, or an extension of the "fuzz" syntax, which is based on LaTeX. Our extensions add prover commands, a paragraph that expresses a theorem, and a means for attaching labels to predicates in an axiomatic or generic box. Z/EVES can read files that have been prepared for the fuzz typechecker.

Z/EVES runs on Linux, Windows and Solaris.

As of July 2002, Z/EVES has been distributed to organizations in 59 countries and 5 continents, and is being used for commercial, academic, and educational purposes.