Greetings, 

  Thank you for your interest in the ZTC tool. ZTC is a type checker
for the Z notation. It is part of an ongoing research project
developing supporting tools for using Z.  Most of the tools are
experimental in nature.  I have used ZTC as an independent tool in my Z
classes, and several Ph.D. students are using ZTC in some projects.

  ZTC accepts two input forms: 
	
  a) LaTeX-zed, LaTeX input using the zed style option defined by 
     Mike Spivey, and 
  b) ZSL, an ASCII version of Z defined by me. With ZSL, you don't 
     have to learn LaTeX to write and type-check Z specifications. 
 	
  In ZSL, a Z schema can be written as follows:

        schema DataDictionary 
          dict : NAME +-> INFO;
          defined : P NAME
        where
          defined = dom dict;
          # defined <= MaxSize
        end schema

or in box form 

        --- DataDictionary ---------------------
        |  dict : NAME +-> INFO;
        |  defined : P NAME
        |----------
        |  defined = dom dict;
        |  # defined <= MaxSize
        ---------------------------------------- 

  ZTC will also perform translations between LaTeX-zed and ZSL.  The
current version of ZTC, version 1.2, conforms the first edition of Mike
Spivey's Z Reference Manual.  We are currently working on a new version
that will conform to the 2nd edition of ZRM.

  ZTC is distributed free of charge for educational and non-profit
uses. In exchange, I would like to hear from you about your experience
in using the tool, and suggestions for improving the tool.

  ZTC can be obtained via anonymous FTP at ise.cs.depaul.edu
(140.192.32.117):

	User name: ftp
	Password:  your e-mail address 
	File: 	   /ftp/dist/ZTC1.2.tar.Z

  It is also available from the Z archive at Oxford via FTP:

	User name: anonymous
	Password:  your e-mail address 
	File: 	   /pub/Zforum/ZTC1.2.tar.Z

You have to uncompress and untar the file on a UNIX system, then
download the files to your PC. All files except ZTC.EXE are ASCII
files.  A floppy disc distribution is also available upon request.

  The distribution includes a User's Guide and some sample input
  files.

  Hope you find ZTC helpful, and I am looking forward to hearing from
you.


Regards,

Dr. Xiaoping Jia
Assistant Professor and Associate Director
Institute for Software Engineering 
DePaul University
Chicago, Illinois, U.S.A.  

Email: jia@cs.depaul.edu