ZTC is a type-checker for Z specification notation. It determines if there are syntactical and typing errors in Z specifications.

ZTC accepts two forms of input: LaTeX with oz or zed packages, and ZSL. Oz and zed are LaTeX packages (style options) developed Paul King and Mike Spivey, respectively, for typesetting Z in LaTeX.
ZSL is an ASCII version of Z designed by the author. ZSL is welcome by students and newcomers of Z who are not familiar with LaTeX, so they can write and type-check Z specifications without the extra hurdle of learning LaTeX. Unlike the SGML based Z interchangeable format proposed by the Z Standard Committee, which is primarily intended for tools not human readers, ZSL is designed to be readable and try to retain the visual appearance of Z specifications as much as possible. ZSL is also useful for ASCII based electronic communications, such as e-mail, involving Z specifications. ZTC can perform translations between LaTeX and ZSL.


Currently the user's guide for ZTC tool is available online in two formats: This document, soon, will be available in HTML format too.

Download site

Please, when you download the tool, fill in the electronic registration form and submit it, so you can receive automatically any information regarding updates, bug fixes etc. The registration form can be found in Registration page.

Contact Info

For further information ot if you wish to contact us, please send an email to fm@saturn.cs.depaul.edu 

Back to Group Page | SE Home


Updated on Aug 12, 1998