The treatment of undefinedness is the main core semantic issue on which I felt it desirable to argue against the position described in Understanding Z (however, see footnote).

The reason for this was that the precise treatment of function applications where the argument is not in the domain of the function, and of definite descriptions where there is no unique individual which satisfies the description, have a significant impact on the complexity of reasoning in the language. Slight variations which are insignificant when considering the language as a specification language can be very important when attempting to construct formal proofs. The main approach adopted in Understanding Z was one of the positions which are awkward for proof without returning any tangible benefit by comparison with approaches which are more convenient for proof.

I constructed for the purpose of discussing this issue, early in 1990, an informal analysis of four different approaches to the treatment of undefinedness in Z, showing how they impacted on the proof rules, and discussing benefits in the clarity and conciseness of specifications.

These viewpoints were as follows:

Blue Book

This refers to the main position described in Understanding Z

Red Book

This refers to my best guess at what was intended in The Z Notation (1st edition, though I don't think that the second has any material differences)

The "Classical" approach

This is the closest to what one might to in standard first order predicate calculus, and gives the simplest proof rules.

The "Ideal" Approach

This is an approach which actually does realise some benefits in conciseness of specification, even though it does pay for this in more complex proof rules than those of the classical approach.

© 1995/6/22 modified 1996/7/25