ZTC: A Type Checker for Z, Version 1.3
	Copyright (c) Xiaoping Jia, 1993. 1994

			 April 1994

ZTC is a type checker for the Z notation. It is a 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 is available on PC and Sun SPARC workstations. 

  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.3, 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

   	Address:   ise.cs.depaul.edu
		   (140.192.32.117)
	User name: ftp
	Password:  your e-mail address 
	Directory: /dist

You will find the following files in the directory:

	ZTC-1.3-DOS.tar.Z	MS-DOS version for IBM-PC
	ZTC-1.3-Sun4.tar.Z	Sun SPARC version for SunOS 4.x
	ZTC-1.3-Solaris.tar.Z	Sun SPARC version for Solaris 2.x
	readme			this file
	
For the PC version, 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. Thank to Mr. Jonathan Bowen, ZTC is now also available on 
the Z archive at Oxford. 
 
  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.