<p>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 <a href="https://en.wikipedia.org/wiki/Z_notation#Standards" rel="nofollow noreferrer">Z notation Wikipedia page</a>.  However, for this particular question, TC1 is not relevant.</p>
<p>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 <span class="math-container">$M$</span> applied outside its domain.  (Can a well-typed specification be written whose semantics depends on <span class="math-container">$M$</span> applied outside its domain?)  I believe this is the thrust of the comment about <span class="math-container">$\mathit{Model}$</span> in Table 27 that states &quot;They are applied only to names in their domains, as guaranteed by well-typedness.&quot;</p>

CC BY-SA 4.0
2021-03-01T23:50:50.490Z
2021-03-01T23:50:50.490Z
Phil Clayton
<p>I may have found an error in the ISO standards document for the Z specification notation, namely <a href="https://www.iso.org/standard/21573.html" rel="nofollow noreferrer">ISO/IEC 13568:2002</a>, &quot;Information technology — Z formal specification notation — Syntax, type system and semantics&quot;.</p>
<p>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 <em>reference expression</em> <span class="math-container">$i$</span>, where <span class="math-container">$i$</span> is a variable name:
<span class="math-container">$$
[[i]]^{\mathcal{E}} = \lambda M : \text{Model} \bullet M\ i.
$$</span></p>
<p>This function is defined for <em>every</em> model <span class="math-container">$M$</span>. But for those models whose domains don't contain the name <span class="math-container">$i$</span> the expression <span class="math-container">$M\ i$</span> is undefined.</p>
<p>Is this, in fact, an error, or do I overlook something? I'd appreciate an authoritative answer; I too can make speculations.</p>

CC BY-SA 4.0
2020-10-11T14:19:58.263Z
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
CC BY-SA 4.0
2020-10-11T14:27:28.743Z
@AndrejBauer You're quite right. I've heard rumors the document can be downloaded free from [this](http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/zdocs/ISO_Z%202002.pdf) address, but I wouldn't know.
Evan Aad
<formal-methods><denotational-semantics>
A possible error in the semantic chapter of the ISO standard for the Z specification notation
Evan Aad
# A possible error in the semantic chapter of the ISO standard for the Z specification notation

(Asked by: username_0 on 2020-10-08)

I may have found an error in the ISO standards document for the Z specification notation, namely [ISO/IEC 13568:2002](https://www.iso.org/standard/21573.html), "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.

**Tags:** formal-methods, denotational-semantics

> **Comments:**
> **username_1**: 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.  
> **username_0**: @AndrejBauer You're quite right. I've heard rumors the document can be downloaded free from [this](http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/zdocs/ISO_Z%202002.pdf) address, but I wouldn't know.  

---

## 1 answers

### Answer by username_2 on 2021-03-01. Score: 1

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](https://en.wikipedia.org/wiki/Z_notation#Standards). However, for this particular question, TC1 is not relevant.

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."


---

