EVES: Documentation

To use EVES, the following documentation will be of help.

• Reference Manual for the Language Verdi:. The reference manual is the definitive (informal) document on Verdi and discusses all the capabilities of the system. Note, the document is a reference manual, not a users' guide. Pedagogical material is sparse and primarily left to an appendix of examples. Available in DVI and PostScript.
• The EVES Library: This document presents a library of reusable mathematical concepts and was initially based on Spivey's Z Mathematical Toolkit. This document is a source of many useful mathematical concepts that can be used in your models and specifications. Available in DVI and PostScript.

The above two documents use the Verdi syntax. The Reference Manual is also available using the s-Verdi syntax. Available in DVI and PostScript.

A tutorial on EVES using s-Verdi is available in DVI and PostScript.

For an example of installing EVES, see the "Software manual for Windows EVES Version 3.0." Available in DVI and PostScript.

Other reports of note include papers on the mathematical semantics of EVES (A Formal Description of Verdi [DVI, PostScript] and an Alternative Semantics for Verdi [DVI, PostScript], a paper on the EVES proof logging facility (EVES Proof Checking and Browsing: Final Report [DVI, PostScript], and papers on the rigorous development of the SPARC Verdi compiler (Structure of the SPARC Verdi Compiler [DVI, PostScript] and A four-phase translation from Verdi to Intermediate Language [DVI, PostScript]).

Though other example uses of EVES are included in the ORA Canada Bibliography, we note the use of EVES to analyze authentication protocols [DVI, PostScript] and the design of a one-way link [DVI, PostScript].

All files have been compressed with UNIX compress.