4
$\begingroup$

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.

$\endgroup$
2
  • $\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$ – Andrej Bauer Oct 11 '20 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 '20 at 14:27
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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