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, &quot;Information technology — Z formal specification notation — Syntax, type system and semantics&quot;.
The possible error is in chapter 15 &quot;Semantic relations&quot;. 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 &quot;Reference expression&quot; 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.
Firstly, in addition to the Standard from 2002, there is also Technical Corrigendum 1 (TC1) from 2007 which fixes a number of issues.  I don't know of any combined document.  Both documents are available free of charge and links to them are available on the Z notation Wikipedia page.  However, for this particular question, TC1 is not relevant.
Section 15 states that &quot;only sentences of concern here are ones that are already known to be well-formed syntactically and well-typed.&quot;.  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 &quot;They are applied only to names in their domains, as guaranteed by well-typedness.&quot;