Date: Mon, 8 Dec 1997 08:20:16 +1000 (EST) From: FSDM Mailing List Subject: Announcing version 1.5 of Z/EVES Content-Type: text Content-Length: 3395 ----------------- Formal Software Development Methods (FSDM) mailing list Submissions and (un)subscription requests to fsdm@it.uq.edu.au or see http://svrc.it.uq.edu.au/pages/FSDM_mailing_list.html ----------------- ORA Canada is pleased to announce the release of version 1.5 of Z/EVES. This version of Z/EVES is available at no cost. Our distribution page http://www.ora.on.ca/distribution.html explains how to obtain the system. The last public release of Z/EVES was version 1.3; version 1.4 was an internal release that was not distributed. Many improvements were made between versions 1.3 and 1.5 of Z/EVES, including: * The documentation has been greatly expanded. The reference manual includes much more information about the effects of commands and the handling of paragraphs. The User's Guide describes what kinds of analysis of Z specifications are important, shows how to use Z/EVES to help in this analysis, and shows how to make best use of the features of Z/EVES. * Support for Z sections has been added. This is a simple modularization facility that allows large specifications to be divided into "sections" that may be processed separately. In addition, there is a facility for "section proofs". * Several new proof command have been added. Commands for finding theorems have also been added. * Support for free types, mu terms, and unique existence has been improved. * The Toolkit conforms to Spivey 2nd edition; many theorems have been added. * The GNU Emacs support has been enhanced, as has the Windows interface. * Error messages have been improved. * Additional examples are included in the distribution. * Technical enhancements have improved the efficiency and robustness of Z/EVES. Z/EVES uses state-of-the-art 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. Z/EVES supports almost the entire Z notation; only the unique existence quantifier in 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). We have automated much of the Z Mathematical Toolkit and included this extended version with the Z/EVES release. Interaction with the Z/EVES system uses 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 SunOS, OS/2, Linux, Windows 3.1, Windows'95 and, with the appropriate compatibility package from Sun, Solaris. Z/EVES has already been used on reasonably large specifications for type checking, schema expansion and domain analysis. These examples have led to plans for commercial use of Z/EVES. As well, Z/EVES has been used to teach Z and theorem proving. More information is available on our Web pages, at http://www.ora.on.ca. Mark Saaltink, ORA Canada ============================================================================== Date: Fri, 16 Aug 96 13:40:43 EDT From: dan@ora.on.ca (Dan Craigen) To: softverf@leopard.cs.byu.edu Subject: Z/EVES Cc: dan@ora.on.ca Sender: owner-softverf@leopard.cs.byu.edu Precedence: bulk Reply-To: dan@ora.on.ca (Dan Craigen) Content-Type: text Content-Length: 3748 All, Since one of the evolving prime uses of Z/EVES is in various courses on software engineering, formal methods or automated deduction, I thought the following announcement may be of interest to readers of this list. Dan Craigen ====================================================================== ORA Canada is pleased to announce the release of the alpha-version of Z/EVES. This version of Z/EVES is available at no cost. Z/EVES supports the analysis of Z specifications in several different ways: o syntax and type checking, o schema expansion, o precondition calculation, o domain checking (are functions applied only on domain?), and o general theorem proving. The range of analysis supports an incremental introduction of Z/EVES capabilities to new users. For example, very 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; and for those that are not, often the generation of the proof obligation is a substantial aid in determining whether a meaningful specification has been written. Z/EVES integrates a leading specification notation with a leading automated deduction capability. Z/EVES supports almost the entire Z notation; only the unique existence quantifier and definite descriptions are not currently supported. The Z/EVES prover provides powerful automated support (e.g., conditional rewriting, heuristics, decision procedures) with user commands that have been found to be helpful in directing the prover in specific ways (e.g., instantiate a specific variable, introduce a lemma, use a function definition). An extended version of the Z Mathematical Toolkit has been developed and is included with the release. Extensive effort has been directed at automating as much of the Toolkit as possible. (Though, some further improvements are in the works.) Interaction with the Z/EVES system uses an extension of the ``fuzz'' syntax, which is based on LaTeX. Our extensions add a means for attaching labels to predicates in an axiomatic or generic box; a paragraph that expresses a theorem; and prover commands. Z/EVES can read files that have been prepared for the fuzz typechecker. While use of Z/EVES is still in the preliminary stages, it has been used on a number of reasonably large specifications for type checking, schema expansion and domain analysis. We are aware of plans for both the commercial and academic use of Z/EVES. Z/EVES will be used to teach Z and/or theorem proving at a number of universities. Z/EVES runs on SunOS, OS/2, Linux, Windows 3.1, Windows'95 and, with the appropriate computability package from Sun, Solaris. A Dynamic Data Exchange (DDE) link between Z/EVES and the Slovakian Z Browser tool has been implemented. Separate acquisition of Z Browser will allow for browsing Z declarations in a Z font as they are added to Z/EVES. Information on Z Browser is obtainable from http://www.comlab.ox.ac.uk/archive/z.html. You may need to contact the developers directly to determine the availability of the DDE enhanced Z Browser. Z Browser is a PC-based tool. (Z Browser is not essential to the productive use of Z/EVES.) ORA Canada will be further improving Z/EVES over the next year. We are particularly interested in receiving your comments on Z/EVES as they will help to direct where we will focus our work. In the near future, an email interest group will be established. For further information on Z/EVES, including technical reports and the distribution procedure, please visit our Z/EVES web page: http://www.ora.on.ca/z-eves/welcome.html. You can also send email to ora@ora.on.ca.