Richer types for Z

The formal specification language Z is strongly typed, but has a rather inexpressive type system in which essentially the only type constructors are power set and Cartesian product. This paper explores the possibility of using a richer type system for extracting information about a Z specification, so that properties like being a function or a sequence become part of the type of an expression. This richer type system adds further type constructors to the sparse set contained in the language definition, and uses properties of Z's library functions to infer information about complex expressions from information about their simpler parts.