Zork: a type-checker for Z from York

Z specifications have been written at York for some years. However, the tool support was minimal: some troff macros to draw schema boxes, and fancy characters that were formed by overlaying existing characters. The aim of the authors´ work was to rectify this situation, without requiring major changes to the existing specifications. They started by improving the typesetting tools by drawing a Z font and improving their troff previewer for the Sun workstations. The authors provided a core for Z by deriving an unambiguous LALR(1) grammar and applying yacc to this grammar to obtain a parser for Zork. They present a small example specification to demonstrate Zork´s capabilities. It especially shows the kind of errors that a type-checker can detect and illustrates how interactive browsing aids the reporting and correction of these errors