Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Wed, 14 Apr 93 14:22:57 EDT
From: bill@ca.on.ora (Bill Pase)
Message-Id: <9304141822.AA06319@alpha.ora.on.ca>
To: info-hol@edu.uidaho.cs.ted
Cc: bill@ca.on.ora
Subject: EVES

EVES was mentioned in the discussion of Set Theory theorem provers.
Here is a brief description of the EVES system.

/bill

----------------------------------------------------------------

NAME: NEVER/EVES

KEYWORDS:  automatic induction, decision procedures, forward rules,
    interactive theorem proving, program verification, rewrite rules

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
senmantics 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 commands.  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 based on
those developed by Boyer-Moore are used for recursive functions to
prevent indefinite expansion of function applications).

The system also 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 use only
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 506
265 Carling Avenue
Ottawa, Ontario K1S 2E1
CANADA

dan@ora.on.ca


USER GROUP

To this point, EVES has been distributed to a small number of sites.
The precursor system, m-EVES, was distributed to about twenty sites.
Two efforts (at the U.S. Naval Research Labs and an effort funded by
Royal Signals and Radar Establishment) using m-EVES to prove
properites pertaining to security have been the major applications of
our technology.

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 control (using command modifiers and low-level inference
commands).  We view the primary advantages of EVES to be its sound
mathematical framework, expressive language, and powerful theorem
prover.  The main weaknesses are that EVES is an isolated tool and
Verdi is certainly not a mainstream development language.

DOCUMENTATION

M. Saaltink, S. Kromodimoeljo, B. Pase, D. Craigen and I. Meisels
Data Abstraction in EVES.
In Proceedings of Formal Methods Europe '93 (FME'93), Odense,
Denmark, April 1993.

D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink.
EVES System Description.
In Proceedings of CADE-11. Saratoga Springs, New York, June 1992.

M. Saaltink.
Z and EVES: A Summary.
In Proceedings of the 6th Annual Z User Meeting, December 1991.
Proceedings in the Springer-Verlag ``Workshops in Computing'' series.

D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink.
EVES: An Overview.
In Proceedings of VDM'91. Noordwijkerhout, The Netherlands, October
1991. 

D. Craigen.
Reference Manual for the Language Verdi.
ORA Canada Technical Report TR-91-5429-09a, September 1991.

M. Saaltink.
A Formal Description of Verdi.
ORA Canada Technical Report TR-90-5429-10a, November 1990.

M. Saaltink.
Alternative Semantics for Verdi.
ORA Canada Technical Report TR-91-5446-02, November 1991.

M. Saaltink and D. Craigen.
Simple Type Theory in EVES.
In Proceedings of 4th Banff Higher Order Workshop, G. Birtwistle (editor),
Springer-Verlag, New York, September 1990.

APPLICATIONS:

Most applications of EVES have been in-house and have been
experimental.  The two substantial efforts, to date, have been the
inclusion of a version of the Z ``Mathematical Toolkit'' (with
model-theoretic proofs of consistency) and of an interpreter for a toy
programming language (called Pico). Other smaller examples have
involved various proofs of program correctness, computer security
properties, and basic mathematical results.

EXTENSIONS/ENHANCEMENTS:

Work will proceed soon on writing a user's guide for EVES and to modify
the syntax from its current Lisp-like form to a form more akin to that
used in set theory.  The programming notation will be based on the
Pascal family of languages. On-going incremental enhancements are being
made to EVES and NEVER.

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.


WHERE TO GET IT:

EVES
ORA Canada
Suite 506
265 Carling Avenue
Ottawa Ontario K1S 2E1
CANADA

eves@ora.on.ca

[Info source, date ]

Dan Craigen, April 1993