Eves System Description

Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink

ORA Canada 265 Carling Avenue, Suite 506

Ottawa, Ontario K1S 2E1 CANADA

Internet: eves@ora.on.ca Phone: (613) 238 7900

March 1992 1 Introduction

The primary purpose of the Eves project^{1} was to develop a verification system, integrating state-of-the-art techniques from automated deduction, mathematics, language design, and formal methods, so that the system is both sound and useful.

The development of Eves has followed two principal directions:

• The design of a specification and implementation language called Verdi. This direction included the development of the formal semantics and the proof system with a demonstration of soundness.

• The implementation of a verification environment. The main component is a theorem prover called Never.

We will only briefly describe the Verdi language, and concentrate instead on the Eves verification environment that has been implemented, particularly the theorem prover component. Additional introductory information may be found in [CKMPS 91] and [CS 90]. [Cra 91] is the reference manual for Verdi, and [Saa 90a] and [Saa 90b] present the mathematical foundations of Eves.

2 Verdi

Verdi is a formal notation that may be used to write programs that are to be verified formally using the Eves verification environment. Consequently, Verdi consists of syntactic forms for expressing specifications (what effect a program is to have), implementation (how a program is to cause an effect), and proofs (justification that a program meets its specification).

Fundamentally, Verdi is a formal notation based on a version of untyped set theory [Fra 68], which can be used to express rigorous mathematical concepts [Saa 91a, Saa 91b]. For example, Verdi can be used to prove theorems of set theory (e.g., Schroeder-Bernstein, Cantor), to prove functional correctness of hardware designs (e.g., n-bit adder), or to prove security-critical properties (e.g., versions of non-interference).

A Verdi theory consists of a current vocabulary and a set of axioms specifying relationships among the names of the vocabulary. Verdi determines an initial theory which introduces names and axioms that can be used by any Verdi program. The Eves database contains a representation of a current theory, heuristic information associated with the theory, and records of complete and partial proofs.

The Verdi syntax is similar to the s-expressions of Lisp. While Verdi is, in general, an untyped language, typing information is necessary for syntactic forms that are to be executed.

3 Never

An integral component of the Eves system is a theorem prover called Never. It is an interactive theorem prover that is capable of performing large proof steps. Features of Never include reduction commands, Boyer-Moore induction, low-level inference commands, and command modifiers that perform variations on reduction commands.

Never is neither a fully automatic nor an entirely manual theorem prover. Although Never provides powerful deductive techniques for the automatic proof of theorems, it also includes simple user steps which permit its use as a system more akin to a proof checker than a theorem prover.

1The development of Eves was sponsored by the Canadian Department of National Defence through DSS contract W2207-0-AF09 and various other contracts. The ORA Canada reference number for this conference paper is CP–91– 6017–44, November 1991.

Combining the manual and automatic functions within a single system creates the possibility of a synergy between abilities of the system (fast and accurate) and the user (the necessary insight).

A user of Eves starts with the initial theory of Verdi, and extends it with Verdi declarations. When a user enters a declaration into the system, the system may generate a proof obligation for the declaration.^{2} The user may then use Never to discharge the proof obligation. The proof may be worked on immediately or it may be deferred. In addition, Eves has a library facility (described in Section 7 below) that allows users to write specifications without proofs and to provide the models with proofs separately.

4 Reduction

The workhorse of Never is the reducer. The reducer reduces a formula to its normal form by an innermost application of simplification, rewriting, and function invocation to each of the subexpressions. A user may tell the reducer to use its full power, only simplification and rewriting, or only simplification, using the reduce, rewrite, and simplify commands respectively. Using command modifiers, a user may tell the reducer to perform variations on reduction commands, such as reducing only certain subexpressions, reducing without variable instantiations, and reducing with specific declarations disabled (e.g., not applying specific rewrite rules). Command modifiers provide tight control over reduction commands, without increasing the complexity of the command set.

The simplifier part of the reducer recognizes propositional tautologies and reasons about integers and equalities. The equality and integer reasoning mechanisms are based on the work of Nelson and Oppen [Nel 81]. A user may extend the simplifier by declaring forward chaining rules (called frules and grules). Using these rules, decision procedures may be added for abstract data types that can be presented as constructor-accessor theories. The system uses forward chaining rules to reason about types used for executable programs. The simplifier tries to instantiate quantified variables when trying to affirm or refute a subformula.

The rewriter applies rewrite rules in addition to performing simplification. A rewrite rule may be conditional, in which case it is only applied if the rewriter shows that the condition is satisfied. Currently, Never does not force the user to enter only terminating sets of rewrite rules although it does detect some cases where rules may loop. Having Never perform checks that warn the user if rewrite rules do not obey some system-defined reduction ordering (such as those used by the conditional term rewriting community) is under consideration. In addition, there is a prototype of a Knuth-Bendix procedure based on Ganzinger’s extension [Gan 87] to handle conditional rewrite rules. The prototype is still being used for experiments to determine its suitability for incorporation into Eves.

The full power of the reducer uses function definitions in addition to performing simplification and rewriting. Non-recursive definitions are always expanded unless they are disabled. For recursive definitions, Never uses heuristics based on those used by Boyer-Moore.

5 Low-Level Inference Commands

Never has commands to perform low-level inference steps. The low level inference commands include commands to instantiate quantified variables, to prenex a formula, to apply axioms manually (axioms include rewrite and forward chaining rules, and those rules associated with function definitions), to perform equality substitution, and to perform a case split.

A user may need to use low-level inference commands to complete a proof. If, for example, the reducer can not find instantiations for quantified variables automatically, the user can give the instantiations explicitly using the instantiate command.

2Generally, the proof obligations are such that, if successfully proven, the declaration results in a conservative extension of the Verdi theory.

Low-level inference commands may be used to search for a proof that the prover was unable to complete automatically. Alternatively, they may be used to step through a proof that was completed automatically, but that the user does not fully understand. The low-level inferences are also useful for debugging conditional rewrite rules that were expected to complete a proof but did not apply. A user may explicitly apply specific conditional rules and then use reduction commands—perhaps with the subexpression command modifier to restrict the reductions to the subexpressions that correspond to the applied rules—to study the prover’s effect upon the result of the application.

6 Induction

Never uses the Boyer-Moore induction technique, extended to handle quantified variables. The heuristics of Boyer-Moore automatically select an induction scheme. A user may override the heuristics by specifying a recursive function term to generate the induction scheme. In addition, Never allows induction in the presence of quantifiers both in the conjecture to be proved and in the recursive function that generates the induction scheme (however, the induction variables must be free in the conjecture). The latter allows one to perform strong induction, by quantifying the recursive call in the function definition.

7 Libraries

The Eves environment supports abstraction and modularity by means of its library facility. The facility allows the user to make, load, edit, and delete library objects. The kinds of objects that may be stored in a library include spec, model, and freeze objects.

A freeze object contains a representation of the Eves system’s state. This can be “thawed” at a later time to restore Eves to that state.

A spec object contains an axiomatic specification. In this specification, it is not necessary to provide complete definitions for any types, functions, or procedures that are declared; instead, axioms can be used to describe their properties. Axioms in a specification do not need to be proved (they are proved in the corresponding model).

A model object contains complete definitions of the types, functions, and procedures declared in the corresponding specification, and contains proofs of all the axioms of the specification. It may contain additional definitions and lemmas that might be used in the main definitions and proofs.

Spec objects may be used as specifications of program modules, in which case the corresponding model defines the implementation of the module; or as a presentation of a mathematical theory, in which case the model demonstrates the soundness of the theory.

The system performs a consistency check between a spec object and its corresponding model object. All symbols declared in the spec object must have a corresponding declaration in the model object. The consistency check is basically syntactic. However, the system allows corresponding declarations to have different heuristics, and it allows stub declarations in spec units.

The library facility is quite flexible: it does not force the user to make spec objects before model objects or vice versa, and it does not force the user to make the corresponding model (spec) object immediately after making a spec (model) object. The user may develop the model objects in a top-down, bottom-up, or mixed fashion.

8 General Remarks

With portability in mind, we wrote the Eves system in a carefully chosen subset of Common Lisp. We have successfully compiled the system under various Common Lisp systems on a number of hardware platforms, including Symbolics 3600, Sun-3, Sun SPARCstation, Apple Mac II, Data General AViiON, and Digital Equipment DecStation.^{3}

The Eves environment has been used on a number of examples, the biggest being a PICO interpreter (about 13,000 lines source) [KP 90]. We translated the specification of a PICO interpreter (from [BHK 89]) into Verdi in the form of specification objects, provided models for them, wrote an imperative program for the interpreter, and verified that the program meets the specification.

We have also built library objects [Saa 91a, Saa 91b] that include most of the “Mathematical Toolkit” as described in Spivey’s Z reference manual [Spi 87]. Many additional laws (beyond those explicitly mentioned in the Toolkit) were needed to complete the proofs of the laws in the Toolkit. During this work, minor errors in the laws were found.

References

[BHK 89] J.A. Bergstra, J. Heering, and P. Klint. Algebraic Specification. ACM Press, New York, New York, 1989.

[BM 79] R.S. Boyer, J S. Moore. A Computational Logic. Academic Press, 1979.

[CKMPS 91] Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase and Mark Saaltink. EVES: An Overview. In Proceedings of VDM ’91. Noordwijkerhout, The Netherlands, October 1991.

[CS 90] Dan Craigen and Mark Saaltink. Simple Type Theory in EVES. In Proceedings of the Fourth Banff Higher Order Workshop. Graham Birtwistle (editor), Springer-Verlag, New York, September 1990.

[Cra 91] Dan Craigen. Reference Manual for the Language Verdi. TR-91-5429-09a, ORA Canada, Ottawa, September 1991.

[Fra 68] Abraham Fraenkel. Abstract Set Theory. North-Holland, 1968.

[Gan 87] Harald Ganzinger. A Completion Procedure for Conditional Equations. In Conditional Term Rewriting System, 1st International Workshop, LNCS 308, Springer-Verlag, Berlin, July 1987.

[KP 90] Sentot Kromodimoeljo, Bill Pase. Using the Eves Library Facility: A PICO Interpreter. FR-90-5444-02, ORA Canada, Ottawa, February 1990.

[Nel 81] G. Nelson. Techniques for Program Verification. CSL-81-10, Xerox Palo Alto Research Center, CA, June 1981.

[Saa 90a] Mark Saaltink. A Formal Description of Verdi. TR-90-5429-10a, ORA Canada, Ottawa, November 1990.

[Saa 90b] Mark Saaltink. Alternative Semantics for Verdi. TR-90-5446-02, ORA Canada, November 1990.

[Saa 91a] Mark Saaltink. Z and Eves. TR-91-5449-02, ORA Canada, Ottawa, October 1991.

[Saa 91b] Mark Saaltink. The Eves Library. TR-91-5449-03, ORA Canada, Ottawa, August 1991.

[Saa 92] Mark Saaltink. Z and Eves: A summary. In Proceedings of the 6th Annual Z User Meeting, held December 1991, Workshop in Computing Series, Springer-Verlag, 1992.

[Spi 87] J.M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1987.

3These systems are the trademarks of their respective manufacturers.