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: