# A possible error in the semantic chapter of the ISO standard for the Z specification notation

I may have found an error in the ISO standards document for the Z specification notation, namely ISO/IEC 13568:2002, "Information technology — Z formal specification notation — Syntax, type system and semantics".

The possible error is in chapter 15 "Semantic relations". This chapter describes the formal semantics of the Z notation. More specifically, the problem is in the following equation appearing in section 15.2.5.1 "Reference expression" on p. 75 that is meant to describe the meaning of a reference expression $$i$$, where $$i$$ is a variable name: $$[[i]]^{\mathcal{E}} = \lambda M : \text{Model} \bullet M\ i.$$

This function is defined for every model $$M$$. But for those models whose domains don't contain the name $$i$$ the expression $$M\ i$$ is undefined.

Is this, in fact, an error, or do I overlook something? I'd appreciate an authoritative answer; I too can make speculations.

• It costs €180 to look at the standard? If that is really the case, perhaps you should expect support from whoever charges money for this thing. We cannot help you here without having access to the document. – Andrej Bauer Oct 11 '20 at 14:19
• @AndrejBauer You're quite right. I've heard rumors the document can be downloaded free from this address, but I wouldn't know. – Evan Aad Oct 11 '20 at 14:27

Section 15 states that "only sentences of concern here are ones that are already known to be well-formed syntactically and well-typed.". In a well-typed specification, the semantics in section 15.2.5.1 should not depend on $$M$$ applied outside its domain. (Can a well-typed specification be written whose semantics depends on $$M$$ applied outside its domain?) I believe this is the thrust of the comment about $$\mathit{Model}$$ in Table 27 that states "They are applied only to names in their domains, as guaranteed by well-typedness."