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

  • $\begingroup$ 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. $\endgroup$ Oct 11, 2020 at 14:19
  • 1
    $\begingroup$ @AndrejBauer You're quite right. I've heard rumors the document can be downloaded free from this address, but I wouldn't know. $\endgroup$
    – Evan Aad
    Oct 11, 2020 at 14:27

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.