The Z specification language is at its heart a typed first-order set theory. It is therefore highly expressive, and supports many different methods or styles of formal specification as well as those which are traditionally associated with Z. The use of Z has been predominantly for model oriented specification, using special features on the language introduced for this purpose and called "schemas". Schemas are essentially just subsets of labelled record types. The Z notation has special features, in the schema calculus and elsewhere, which support the use of schemas as model oriented specifications of operations. There are however, other ways of using the language which diverge from this norm, and either fail to use schemas, or make more limited use of the schema notation.

© created 1995/5/24 modified 1996/7/25