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