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.

Download Z2SAL Translator Tool (Live Version)

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.

• Z2SAL Translator, version 1.13 for Java 1.6SE (build: 20 July 2012)
• Z2SAL Translator, version 1.11 for Java 1.6SE (build: 18 July 2012)
• Z2SAL Translator, version 1.9 for Java 1.6SE (build: 27 June 2012)

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 Z Reference Manual, 2nd.ed., J M Spivey et al., 1998
• The ISO Z Standard (ISO/IEC 13568), 2002
• A Guide to the zed Style Option, J M Spivey, 1990
• Printing Z and Object-Z LaTeX Documents, P King, 1990
• The Z of ZeTa (v1.5), R Büssow and W Grieskamp, 2000

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 zed.sty LaTeX style for Z, © Mike Spivey, University of Oxford, 1990
• The oz.sty LaTeX style for Z and Object-Z, © Paul King, University of Queensland, 1990
• The esz.sty LaTeX style for proto-ISO Z, © Robert Büssow and Wolfgang Grieskamp, Daimler, 1997

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).

• The SAL Language Manual, L de Moura, S Owre and N Shankar, 2003
• SAL: Tutorial (tools, environment), L de Moura, April, 2004
• SAL: Tutorial (tools, environment), L de Moura, November, 2004

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:

• Z2SAL Bug Report — use to report any errors with the tool.
• Z2SAL Feedback — use to give general feedback on the tool.