An Algorithm for Type−Checking Z

Abstract

We present an outline of an algorithm for type-checking Z specifications and determining appropriate error messages. The algorithm understands an abstract syntax of Z as given by J.M. Spivey, and is similar to the one implemented in the Forsite prototype specification support environment. The outline presented here is intended to serve as a. brief introductory overview to implementing a Z type checker, and to elucidate important and subtle details involved in type checking Z. We do not discuss user interface or performance issues such as display of error messages or representation of data structures. The outline is itself described in Z.