@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
NAME: EVES/NEVER

KEYWORDS:  automatic induction, decision procedures, forward rules,
    interactive theorem proving, program verification, rewrite rules,
    proof logging, proof checking, formal methods, Verdi, Z,
    high integrity applications.

DESCRIPTION: 

SEMANTICS:  

EVES uses untyped first-order logic, without the conventional
distinction between terms and formulas.  The axioms of
Zermello-Fraenkel set theory are included in the EVES "initial
theory."

EVES has a mechanism for defining new functions.  Every declaration
must be proved to define a conservative extension of the theory in
which it appears.  There is also a library system that allows theories
to be combined.  Every axiomatic theory in the library must have a
corresponding "model" that establishes its soundness.

EVES also allows for procedure definitions. Procedures are specified
using pre and post assertions, and are proved by proving certain
"proof obligations" determined from the procedure definition and its
annotations.

The semantics of Verdi follows the usual first-order model theory,
with simple extensions to handlle definitions and libraries.  The
semantics of procedures is defined by a denotational definition
that is fully integrated with the model theory for the rest of Verdi.

DEDUCTIVE MACHINERY:

Proofs are done in the system using commands that perform
equivalent-preserving transformations on the current formula.  The
workhorse of the theorem prover, the reducer, is invoked using the
SIMPLIFY, REWRITE, or REDUCE command.  The SIMPLIFY command instructs
the reducer to attempt to replace the current formula with an
equivalent formula which the reducer considers to be simpler.  The
reducer performs propositional simplification (propositional
tautologies are always detected), reasons about equalities,
inequalities, integers, and quantifiers, as well as applying forward
rules (rules that are specifically introduced to extend the
simplifier).  The REWRITE command causes the reducer to apply rewrite
rules in addition to the above.  The REDUCE command causes the reducer
to expand function applications using their definitions as well as
performing everything that is done under REWRITE. (Heuristics
gneralized from those developed by Boyer-Moore are used for recursive
functions to prevent indefinite expansion of function applications.)

The system provides the user with commands to perform simpler
inferences (such as explicit instantiation of a quantified variable)
as well as a command to perform Boyer-Moore-style automatic induction.
In addition, command modifiers may be used to allow the user to have
finer control over the effects of a command (they are intended mainly
for reduction commands).

DYNAMICS:

Theories are built up incrementally by entering declarations into
the system.  There may be a proof obligation associated with a
declaration, e.g., for a recursive function declaration, the user must
show that the recursion terminates, and for an axiom declaration, the
user must show that the body of the axiom declaration is in fact a
theorem.  The proof obligation may be worked on immediately after the
declaration is entered, or the user may proceed with other
declarations and come back to the proof later.  However, to prevent
circularity of reasoning, the proof of a declaration may only use
axioms that were introduced by earlier declarations.  To perform a
proof, commands described in the previous section may be used.  In
addition, the user may undo the effects of proof commands as well as
declarations (the undoing is strictly last-in-first-out).

PERSISTENCE:

The system retains partial and complete proofs of declarations.  In
addition the current theory may be saved as a library unit.  The kind
of library unit that can be loaded into the system is called a spec
unit.  For a spec unit, proofs do not have to be completed and are in
fact discarded.  Information hiding is supported by allowing stub
declarations in a spec unit.  Proofs must be completed and are saved
in the corresponding model unit, and a consistency check is performed
between the spec unit and the model unit.

An incomplete theory development may be saved as a freeze unit.
For a freeze unit, proofs do not have to be completed but partial
and complete proofs are saved.  The user may later thaw the unit
which causes the state of the development to be completely restored
(including the partial and complete proofs).

Saved theories may be undone by deleting library units.  The
system keeps track of the dependencies among library units since
the deletion of a unit may require the deletion of other units
that depend on the deleted unit.

CONTACT PERSONS: 

Dan Craigen
ORA Canada
Suite 100
267 Richmond Rd.,
Ottawa, Ontario K1Z 6X3
CANADA

dan@ora.on.ca


USER GROUP

To this point, EVES has only been distributed to a small number of
sites. Various establishments (government and academic) have been
using EVES on experimental applications. The U.S Naval Research Labs
and the U.K. Royal Signals and Radar Establishment (now DRA), used
EVES technology in security-critical applications. Currently, EVES is
being used (by ORA Canada and CGI), under a contract to the Canadian
Atomic Energy Control Board, for the development of a (pedagogical)
boiler control and shutdown system. EVES is being used by various
universities, not only for R&D, but for teaching formal methods.

In the Fall/Winter'95, we intend to make EVES and Z/EVES (see below)
available over the Internet.

PRAGMATICS

The theorem prover combines the power of its automatic capabilities
(embodied in the reduction commands) with the ability of the user to
have fine-grained control (using command modifiers and low level
inference commands). We view the unique attribes of EVES as being the
combination of (i) an expressive formal specification and programming
language, (ii) practical automated deduction support, (iii)
mathematical soundness, (iv) rigorous tool development, and (v)
availability on workstations and PCs.  As per weaknesses, the main
weaknesses are that EVES is an isolated tool and Verdi is certainly
not a mainstream development language. As described below, our current
work on developing a Z front-end to EVES is meant to ease technology
transfer and to provide a unique integration of European and North
American capabilities.

DOCUMENTATION

An annotated bibliography of EVES reports is available at our Web site
(http://www.ora.on.ca/). Most of our reports and publications are
available in postscript or dvi formats.

Also available at the Web site, are five introductory examples on how
EVES was used across various computing science areas, including
computer-security, hardware verification, and ring theory.

APPLICATIONS:

During 1995-7 a series of software engineering and critical systems
applications are either planned or underway. See our Web site
(http://www.ora.on.ca/) for updated information.

EXTENSIONS/ENHANCEMENTS:

Work is underway to integrate the Z notation with EVES. Such an
integration brings together state-of-the-art formal methods techniques
from Europe and North America. In Z/EVES, Z is extended to included
paragraphs for stating theorems and for performing proofs. Z/EVES will
be available in the Fall/Winter 1995. Work is also progressing on
developing an independent proof checking capability, through which the
proofs discovered by EVES/NEVER are validated. Work was recently
completed in defining the Verdi inference rules and for logging, in
terms of those rules, the proofs discovered using EVES/NEVER.  During
1996/7, ORA Canada will be involved in a number of applications
involving EVES. Other work at developing a general formal methods
environment are also progressing.

RESOURCE REQUIREMENTS:

The system is implemented in a disciplined subset of Common-Lisp.  It
currently runs under KCL (Kyoto Common Lisp), AKCL (Austin Kyoto
Common Lisp), and Allegro Common Lisp on Sun workstations.  On a Sun-3
workstation, 16Mb RAM or more is recommended.  On sparcstations, 32Mb
RAM is recommended. The system is also available on PCs (running DOS).
For a PC, one should have, at least, a 486 processor and 8Mb RAM.


WHERE-TO-GET-IT:

EVES
ORA Canada
Suite 100
267 Richmond Rd.,
Ottawa, Ontario K1Z 6X3
CANADA

ora@ora.on.ca

[Info source, date ]

Dan Craigen, August 1995


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%