The Treatment of Undefinedness in Z

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.

Understanding Z does discuss alternative treatments of undefinedness, and Mike Spivey has made it clear that he does not consider the book to have taken a position on which of these should be adopted. Nevertheless, it is convenient to talk of the position described in detail in the main body of the semantic account in Understanding Z as the position defined by that work, and it should be understood that in doing this I am not intending to contradict Spiveys own account of his intentions.

UP HOME © RBJ 1995/6/22 modified 1996/7/25