Zadok User Guide
Abstract
This document is a guide for users of Zadok, the Z syntax and typechecker developed by the SCEIP Unit at RSRE. It is assumed that users of this tool may not be familiar with the Perq computer operating with the Flex system, so an introduction to the use of Flex is given. Some knowledge of Z is assumed. This Guide also introduces the keyware software developed by the SMITE team at RSRE which is used with the Z tool. Other topics covered are how to use the Z editor; how to run the Z typechecker and correct errors it may find in your file of Z; and how to print your file using a PostScript printer. Section 6 discusses two issues relating to the Z language, namely differences between the syntax used by the typechecker and that given in Spivey's reference manual (Spivey88), and the style of language adopted by the typechecker. The final section describes some known problems with the Z tools, including the editor, and gives advice on how to deal with these. The annexes contain the Z symbols used by the editor, and what they mean, the Z library of basic mathematical constructs used by the typechecker and the Z syntax used by the tool. (rh)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1990
- Accession Number
- ADA222071
Entities
People
- G. P. Randell
Organizations
- Royal Signals and Radar Establishment