Z/EVES Eclipse prover IDE

Community Z Tools provide an Eclipse-based IDE and integration with Z/EVES theorem prover. This extends the development of Z specifications in CZT with theorem proving and verification capabilities.

Z/EVES Eclipse provides a modern environment to use the Z/EVES theorem prover. It is an alternative to the original Z/EVES UI, which is no longer in development and has issues when used with modern operating systems.

Z/EVES Eclipse brings the Z/EVES theorem prover to a modern IDE and supports all Z/EVES functionality: writing and sending proof commands to the prover, viewing proof output, querying lemmas, section management, etc.

Getting started

To get started with Z/EVES in Eclipse, use the zeves dialect and the Z/EVES perspective, configure and launch the Z/EVES prover, and submit your proof script commands to the prover. The following steps provide slightly more details.

Get Z/EVES Eclipse: it comes together with CZT IDE. Alternatively, install it from the CZT update site.
Setup your Z/EVES project.
Make sure to select the zeves dialect in Z compiler preferences!

Otherwise Z/EVES statements (e.g. proof commands) will not be recognised. Reload the open editors after selecting the dialect.
Select the Z/EVES perspective via menu: Window > Open Perspective > Other… > Z/EVES.

The Z/EVES views will be opened and arranged - they give a proof-centric view of developing Z specifications.
Configure and launch the Z/EVES prover launch configuration in Run > External Tools > External Tools Configurations > Z/EVES.
Open your Z/EVES specification.
Submit specification contents to the Z/EVES prover using the toolbar buttons . These submit the next command to the prover, go back one command or submit everything up to the cursor, respectively.

For your convenience, use keyboard shortcuts for these commands: Shift + Ctrl + Up/Down/Enter (use the Cmd key instead of Ctrl on Mac OS X).
The submitted commands are highlighted. Use the Z/EVES Output view to inspect prover output (e.g. outstanding goals) at the selected command.
Select Force Unicode in the Z/EVES Output view toolbar to show unicode-rendered prover output.
Write new proof commands directly to the specification; or use menus available in the Z/EVES Output view to drive the theorem prover.
Refresh other Z/EVES views (e.g. Theorems) to get the newest information from the prover.

Features

Z/EVES Eclipse supports all Z/EVES features and provides a convenient integration with other Community Z Tools. Some of the features are listed below:

Z/EVES launch configurations
Z/EVES dialect for typesetting Z specifications in Z/EVES style + support for proofs and proof commands.
Actions to submit proof commands to Z/EVES either one-by-one, or “everything up to the cursor”.
Undo when editing: when you edit the document, the Z/EVES prover will be rolled back to the edit point (no need to undo manually).
Markers for erroneous Z/EVES commands are displayed in the specification.
Asynchronous proof output display: select the command to view its results or outstanding goals in the Z/EVES Output view.
Support viewing Z/EVES output in Unicode even when developing in Z LaTeX.
Select proof commands from the menus in the Z/EVES Output view.
Context-specific proof commands are available via context menu in the Z/EVES Output view.
Section management (not supported by the original Z/EVES UI!)
- Develop your Z/EVES specification using Z sections: all dependencies will be submitted to the prover as well.
- Undo the whole section in the Z/EVES view.
View theorems, axioms and their proof status in the Theorems view.

Read more about the CZT and Z/EVES Eclipse features in the documentation.