Translation-Based Tools for Z

Model-checking and refinement checking

You are here: Z2SAL Home / Download /
Department of Computer Science

The Z2SAL Download Centre

The public beta-version of our Z to SAL translation tool is available here. The tool is provided as a Java application with a simple user interface. Currently, the tool has two operating modes, in which it will either translate a single Z specification for model-checking purposes, or will translate a pair of Z specifications for refinement checking purposes. The translated output is placed in the same directory as the source. Please consult the Z2SAL User Guide for further information on how to use the tool. You may download a live version (subject to changes), or a previous stable release. We also have an internal alpha-version of the tool, which translates more Z features than the public version, but which we have not yet thoroughly tested.

Previous Releases

Please click to download a specific release, as a Java archive (jar) file. The translator may be launched by double-clicking on the jar-file's icon, or using the   java –jar filename   command-line utility.

The Z to SAL translator accepts files containing marked up Z, in several possible LaTeX Z styles, and outputs one or more files in the SAL format. For further information on expected file formats, and how to use the tool, please consult the Z2SAL User Guide.

Resources for Z, SAL and LaTeX

We have archived a number of useful Z documents and LaTeX style files, for those wishing to create their own Z specifications. The standard reference for Z was the Z Reference Manual; additions may have since been agreed in the ISO-Z standard.

The original LaTeX style file was Mike Spivey's zed.sty; this has since been extended several times. A popular LaTeX style is Paul King's oz.sty, which also supports the Object-Z extension.

The latest documentation for the SAL tool suite is available from SRI's website for the Symbolic Analysis Laboratory. Below, we mirror a few of their earlier tutorial guides. (Note: the SAL tool suite is updated on a regular basis; these may become out of date).

Send Feedback

We are keen to receive feedback about the performance of the tool. Please feel free to contact us, either to report any faults, or to give general feedback on the behaviour of the Z2SAL translator:

Before sending in a new bug report, please consult the page listing Known Bugs.

Regent Court, 211 Portobello, Sheffield S1 4DP, United Kingdom