From rinehuls@Radix.Net Fri Jan 7 23:49:20 2000 Received: from mail1.radix.net (mail1.radix.net [207.192.128.31]) by dkuug.dk (8.9.2/8.9.2) with ESMTP id XAA24954; Fri, 7 Jan 2000 23:49:19 +0100 (CET) (envelope-from rinehuls@Radix.Net) Received: from saltmine.radix.net (saltmine.radix.net [207.192.128.40]) by mail1.radix.net (8.9.3/8.9.3) with SMTP id RAA25853; Fri, 7 Jan 2000 17:42:57 -0500 (EST) Date: Fri, 7 Jan 2000 17:42:55 -0500 (EST) From: William Rinehuls Reply-To: William Rinehuls To: sc22info@dkuug.dk cc: keld simonsen Subject: SC22 N3048 - Vote Summary on FCD 13568: Z Specification Language Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by dkuug.dk id XAA24954 __________________ beginning of title page _________________________ ISO/IEC JTC 1/SC22 Programming languages, their environments and system software interfaces Secretariat: U.S.A. (ANSI) ISO/IEC JTC 1/SC22 N3048 TITLE: Summary of Voting on FCD Ballot for FCD 13568: Information technology - Programming languages - Z Specification Language DATE ASSIGNED: 2000-01-07 SOURCE: Secretariat, ISO/IEC JTC 1/SC22 BACKWARD POINTER: N/A DOCUMENT TYPE: Summary of Voting PROJECT NUMBER: JTC 1.22.45 STATUS: WG20 is requested to prepare a Disposition of Comments Report and make a recommendation on the further processing of the FCD. Please note that the comments accompanying the affirmative vote from the United Kingdom Member Body are contained in document N3049. ACTION IDENTIFIER: FYI to SC22 Member Bodies ACT to WG20 DUE DATE: N/A DISTRIBUTION: Text CROSS REFERENCE: N2982, N3049 DISTRIBUTION FORM: Def _____________ end of title page; beginning of general summary ________ SUMMARY OF VOTING ON Letter Ballot Reference No: SC22 N2982 Circulated by: JTC 1/SC22 Circulation Date: 1999-09-01 Closing Date: 2000-01-04 SUBJECT: FCD Ballot for FCD 13568: Information technology - Programming languages - Z Specification Language ---------------------------------------------------------------------- The following responses have been received on the subject of approval: "P" Members supporting approval without comments 5 "P" Members supporting approval with comments 1 "P" Members not supporting approval 3 "P" Members abstaining 3 "P" Members not voting 9 "O" Members supporting approval without comments 1 ------------------------------------------------------------------------ Secretariat Action: The comment accompanying the abstention vote from Denmark was "Due to lack of Danish expertise." The comment accompanying the abstention vote from the Netherlands was: "Due to lack of expertise." The comments accompanying the negative votes from Canada, Japan and the United States of America are attached. The comments accompanying the affirmative vote from the United Kingdom are contained in document SC22 N3049. WG20 is requested to prepare a Disposition of Comments Report and make a recommendation on the further processing of the FCD. _________end of general summary; beginning of overall summary _______ ISO/IEC JTC1/SC22 LETTER BALLOT SUMMARY PROJECT NO: JTC 1.22.45 SUBJECT: FCD Ballot for FCD 13568: Information technology - Programming languages - Z Specification Language Reference Document No: N2982 Ballot Document No: N2982 Circulation Date: 1999-09-01 Closing Date: 2000-01-04 Circulated To: SC22 P, O, L Circulated By: Secretariat SUMMARY OF VOTING AND COMMENTS RECEIVED Approve Disapprove Abstain Comments Not Voting 'P' Members Austria ( ) ( ) ( ) ( ) (X) Belgium (X) ( ) ( ) ( ) ( ) Brazil ( ) ( ) ( ) ( ) (X) Canada ( ) (X) ( ) (X) ( ) China (X) ( ) ( ) ( ) ( ) Czech Republic (X) ( ) ( ) ( ) ( ) Denmark ( ) ( ) (X) (X) ( ) Egypt ( ) ( ) ( ) ( ) (X) Finland (X) ( ) ( ) ( ) ( ) France ( ) ( ) (X) ( ) ( ) Germany ( ) ( ) ( ) ( ) (X) Ireland ( ) ( ) ( ) ( ) (X) Japan ( ) (X) ( ) (X) ( ) Netherlands ( ) ( ) (X) (X) ( ) Norway ( ) ( ) ( ) ( ) (X) Romania ( ) ( ) ( ) ( ) (X) Russian Federation (X) ( ) ( ) ( ) ( ) Slovenia ( ) ( ) ( ) ( ) (X) UK (X) ( ) ( ) (X) ( ) Ukraine ( ) ( ) ( ) ( ) (X) USA ( ) (X) ( ) (X) ( ) 'O' Members Voting Korea Republic (X) ( ) ( ) ( ) ( ) _________ end of detail summary; beginning of Canada comments _______ COMMENTS TO SUPPORT CANADA'S NEGATIVE VOTE ON: FCD13568 (JTC1/SC22 N2982 ) Summary: Canada votes NO with comments. If numerous major and minor difficulties are satisfactorily addressed in a subsequent re-draft of the proposed FCD, Canada's vote would change to YES. Reasons: 1. A document with this large a number of changes from the previous version probably ought not to be presented as an FCD, as the risk of introducing errors in making such sweeping alterations is very high. 2. The document shows evidence of requiring more careful proofreading for clarity and correctness of English before becoming acceptable as a standard. This is especially so in the earlier sections. 3. There are major issues in the technical specification that need to be dealt with before proceeding to FDIS, as they cannot be adequately dealt with once that happens. Comments PART A Comments on the technical contents of the Document Comments labeled "[major]" must be addressed before the draft is acceptable, as they address issues of consistency between implementations and portability of specifications (which is the overall goal of standardizing Z). Section 3 Terms and definitions 1) [minor] The term "theorem" is not used, and so the definition is not needed. Section 4 Symbols and Definitions 2) [minor] Clause 4.2, Mathematical Metalanguage Some functions defined in this clause are only defined partially, e.g., addition, cardinality, first, second, and application. This might lead to some question about the meanings of metalanguage expressions involving these names. It is trivial to define these functions as total, and removes the questions. 3) [minor] Clause 4.2.5.5 defines the notation "f x" to be application. However, there is room for confusion, as other metalanguage notations (e.g., "dom R") match the pattern. Perhaps it would be best to define a metalanguage operator to denote function applications (e.g., Quine's 'f " x') 4) [minor] Table 23 defines "Theory" in a very nonstandard way. A theory is not usually a function, or a set of models. "SectionEnvironment" or "SectionModels" might be less confusing. Section 5 Conformance 5) [minor] Clause 5.1 The picture here is a bit oversimplified. Lexical analysis is dependent on a lexical context, that itself depends on fixity paragraphs and sections (i.e., a section's parents must be determined to establish the proper lexical environment). Indeed, the reordering of sections is specified in the type rules, but not for lexical analysis, but it is necessary for lexical analysis. It may also be necessary for the mark-up phase; see the comments on Annex A. Some of the issues are mentioned in Clause 5.3, but reordering does not seem to be discussed. 6) [minor] Clause 5.1. Might the "instantiating" stage also be partial? Consider the specification a[X] == 1 b = a After the first paragraph, the generic type of a is [X] Given Arithmos. So for the paragraph b == a, we will have a transformation to AX [b == a] END and then to AX [[b:{a}]] END There does not seem to be an expression rule for [[b:{a}]]. We will work out the result for the paragraph AX [b:{a}] END. Now with Sigma being the appropriate environment (with the declaration of a in effect), we have Sigma[a] = [X] Given Arithmos, which I'll call "g". Rule 13.2.5.1 says ------------------------ Sigma |- a : tau where tau = g, g[tau_1] Clause 14.3 states that instantiation is a metafunction, so we suppose that "([X] Given Arithmos)[tau_1]" is not supposed to appear literally in the deduction; instead, we determine its value. This value is simply Arithmos, so we have ------------------------ Sigma |- a : tau where tau = g, Arithmos Note: there are no type variables besides tau here, and tau is constrained. Now we hit one of the confusing points, because we have a funny looking tau (combining a generic type and a type), but the examples show that we carry on with the type and save the generic type for a later phase. So, we have ------------------------------------- 13.2.5.1 Sigma |- a : Arithmos ------------------------------------- 13.2.5.3 Sigma |- {a} : P Arithmos -------------------------------------- 13.2.5.13 Sigma |- [b:{a}] : P [ b: Arithmos ] --------------------------------------- 13.2.3.2 Sigma |- AX [b:{a}] : [b: Arithmos] The type rules are satisfied; even the note in Clause 13.33.2 is satisfied as the only well-typedness condition concerns tau, and it has a unique solution. Hence, the generic instantiation phase (Clause 14.4) will fail. 7) [minor] Clause 5.2.4 Mathematical toolkit conformance, is rather strict, in that it precludes a toolkit with sections having different parents. Perhaps a proof tool should be allowed, say, to have the number section use the function section as a parent. Section 6 Z Characters ---------------------- 8) [minor] Clause 6.4.7 Renderings of Z characters, states "tokens shall be rendered consistently throughout a specification" . Does this rule constrain Z tools or Z specifications? That is, if we write (in LaTeX) "\dom f = dom g", is the specification in error? Must a tool reject it? Section 7 Lexis --------------- 9) [major] The whitespace rules are a bit sloppy. e.g., "_a" might be the underbar token followed by a WORD. Space is required (lest it be lexed as a WORD). Similarly, spaces might be required between a PRE and a WORD, and so on. The lexis does not indicate whether "if'" is a valid NAME, or is instead the if token followed by a stroke. This area is a prime candidate for tool variation, and should be made explicit in the standard. 10) [minor] "NUMBER" tokens should more properly be called "NUMERALS". 11) [major] The lexis does not allow some of the declarations of the toolkit. For example, in Clause B.8.2 we have the fixity declaration function 90 ( _ /^ _ v/ ) which is not allowed - the arrows would need to be words (but are not, as up and down arrows in words must be balanced, according to 7.3). 12) [minor] In Clause 7.3, it would be useful to specify a minimal level of required support for section names. 13) [minor] Clause 7.5 Newlines should say what the rules are if the newline is the first or last character of an entire specification (in which case the references to "the token" are not meaningful). Section 8 Concrete Syntax ------------------------ 14) [minor] Clause 8.1 states that terminals are not used in the syntax, so as not to impose any particular markup. However, markups are defined to determine sequences of Z characters, so terminals that are sequences of Z characters would impose no bias. 15) [minor] Note 1 (of Clause 8.1) is irrelevant: any grammar has an unambiguous larger grammar. Further, since e.g., conjunction is ambiguous, the claim is suspicious. 16) [major] Clause 8.4's rule "Operator template paragraphs shall not give different associativities to operators at the same precedence" is not as explicit as necessary. Does this apply to a complete specification, or only to related sections? [minor] The above rule is also annoying, in that it requires specifiers to keep track of which precedence numbers are associated with which associativity. An alternative rule requiring parentheses in cases where a phrase is bound left and right with equal precedence might be nicer, if it could be formulated precisely. (Standard ML has this rule.) 17) [major] Clause 8 does not resolve all ambiguity in the grammar. For example, "pre 1 post", where pre and post are operators at the same precedence level, might associate either way. (Perhaps a "pre" token should be considered left associative and a "post" token right associative.) There appears to be a further a problem in the fact that Boolean operations on schemas have a different precedence than those for predicates. That is, suppose S, T, and U are schemas, and we write the predicate S /\ T \/ U. We expect that to be (S /\ T) \/ U, whether the operations are predicate ops or schema ops. But it is possible to form S /\ (T \/ U), where the conjunction is a predicate conjunction and the disjunction is the (higher-precedence) schema disjunction. 18) [major] Clause 8.4 is not completely clear in how "if they can be" is to be interpreted. For example, in the expression "\theta S ' '", either stroke can be interpreted as part of the binding interpretation, but they cannot both be so interpreted. Which of the two interpretations is to be chosen? 19) [major] The working of mixfix is not fully spelled out. For example, one can write generic 30 leftassoc ( _ a _ b _ ) generic 40 rightassoc ( _ c _ d _ ) so that a and c are EL tokens, b and d are ERE tokens, then declare X a Y c Z == X X b Y d Z == Y The syntax apparently also now allows the further declaration X a Y d Z == Z What precedence rules apply to this operator? Is it left or right associative? Is the precedence 30 or 40, or something else? There are two simple resolutions to this problem: 1. Record the operator template origin of each token, and disallow mixing. Then "_ a _ d _" is illegal, as the origins of "a" and "d" differ 2. Require all the tokens in a mixfix form to have the same precedence and associativity. So the above example would not be allowed, but would be OK if the second declaration were "generic 30 leftassoc ( _ c _ d _ )" Section 9 Characterization rules -------------------------------- 20) Clause 9.1 presents what appear to be transformation rules. These should simply be equations in the metamathematics. Otherwise, the transformations would be possible only if concatenation were in the object language. Section 10 Annotated Syntax --------------------------- 21) [major] Clause 10.2: It is highly confusing to use \tau both at the object level, as a "variable type", and at the metalevel as a metavariable. Some different symbol should be used for object level "variable types", if they are indeed retained. Section 11 Prelude ------------------ 22) Clause 11 is not required. A specification needs to be type checked with respect to a type environment mapping \arithmos to the type "\powerset given \arithmos", and the type of a numeral is "given \arithmos", and "\powerset" needs to have prefix generic fixity. The semantics of a specification needs to be in an initial environment mapping \arithmos to some superset of the integers, and needs to give each numeral its base 10 interpretation. These are easily specified in clauses 13 and 16 respectively. We are not sure what benefit is derived from specifying this initial environment syntactically rather than semantically. Section 12 Static transformation rules -------------------------------------- 23) [minor] The grammar and prelude declarations admit "\power _" as an OPNAME. For example, we can write the expression (%P _)[%N]. The transformation rules do not appear to handle this. 24) [minor] Clause 12.2.8.1 (and others?) glue template parts together with a bowtie character. Traditionally, underbar has been used for this purpose. There is no obvious reason not to follow established practice, e.g., transforming "a + b" to "_+_ (a,b)" 25) [major] the "variable types" introduced, e.g. in 12.2.6.1, must be different for each application of a transformation rule. (Otherwise, for example, "a, b: \num; c, d: \power \num" will fail because \tau_1 is overconstrained). Section 13 Type inference rules ------------------------------- 26) [major] How the rules are applied is not clearly spelled out, although some if it can be inferred from notes and the examples in Annex D. However, there should be normative text describing it. We expected something along the lines of this: the parser produces an abstract syntax tree; the type rules let us infer facts of the form $\Gamma \entails^P ast$ or $\Gamma \entails^E ast \fatsemi \tau$, and a specification $s$ is well typed if we can infer $\emptyset \entails^S s$. In this scheme, the metavariables and ellipses appearing in the rules are just a way of describing a whole set of specific inferences allowed by the rule. What we have is quite different, in that we are apparently supposed to have instances of these rules with type variables in them, then derive equations between variable types, then solve the equations. We are not quite sure how these equations should look or be derived. Most of the examples in Annex D illustrate the plan sketched above. The example of D.8 does not; instead each expression node is decorated with two types (involving "variable types") and we infer that the type constraints take the form of equations between the two type expressions on each node. The types decorating the expression nodes are apparently just freshly renamed instances of the type expressions appearing in the type inference rules. This is understandable in many cases, but is not clear in the case of tuples selection (rule 13.2.5.7) or binding construction (rule 13.2.5.9), because of the ellipses there. Evidently, we have a choice of many different possible expressions to annotate the selection node with (i.e., \tau_1 \cross \tau_2, or \tau_1 \cross \tau_2 \cross \tau_3, or ...) How do we choose? We think there may be as many as four annotations on a node of the parse tree. Various rules in Clause 12 (e.g., 12.2.6.1 or 12.2.10.3) might add a variable type. Type inference rules might apparently add two more (one in a conclusion, one an a hypothesis). Finally, rule 13.2.5.1 annotates with a pair consisting of the normal type and an uninstantiated type (used in a later phase). Furthermore, we have some cases where there are nodes in a typing derivation that are not present in the original parse tree (e.g., one of the antecedents of a derivation for "\theta S '" can be about "i'", which need not appear explicitly anywhere in the specification. So, type checking is not just about decorating a parse tree. In short, the reader may be unable to understand the type rules in sufficient detail to apply them, or to know how to check their accuracy. 27) [major] The rule in 13.2.2.1 that tries to force generic inference to succeed for each prefix of a section's parents does not work. For example, a specification S == [a, b: \emptyset] T == [S | a = 1] will be accepted because earlier phases have associated a type variable \tau_1 with the \emptyset. Unless this variable is regenerated for the "\Lambda \entails^s s" hypothesis, we have a problem. In detail, the specification above is transformed to S == [a: \emptyset \fatcolon \tau_1 ; b a: \emptyset \fatcolon \tau_1] T == [S | a = 1] and we have a large type deduction tree. However, it seems clear that \tau_1 is fully constrained in this tree. 28) [major] Theta terms are not properly handled. We can have c[X] == X S == [c: \power \num] AX \theta S \in S the predicate \theta S \in S is well-typed as we can deduce the subgoal \Sigma \entails^E c \fatcolon \power \num in rule 13.2.5.9 Rule 15.2.5.2 now suggests rewriting \theta S to \lblot c == c \rblot but here we have lost the information about how the generic actuals were inferred, and there seems to be no way to end up with the necessary \lblot c == c[\num] \rblot Another problem arises in the following example T == [x: \num] U == [\Delta T: \power (\Delta T)] \theta U \in U the type rules accept "\theta U", because we can infer "\Delta T \fatcolon ...". Rule 15.2.5.2 again applies, to the final predicate, and we get \lblot \Delta T == \Delta T \rblot \in U According to the diagram in Clause 5.1, we are now past the stage where rules of 13.2.5.1 could apply, so we are stuck with the expression "\Delta T", which the semantic rules will not handle correctly. 29) [minor] Clause 13.2.3.4 should define $\Sigma_0 = \Sigma \oplus \{ f_1 \mapsto \power (Given f_1), \dots \}$ 30) [minor] Clause 13.2.5.20 does not need to require the old names to be distinct. The rule as written, with the distinctness constraint removed, works perfectly well and is a bit more general. The semantic equations also work as written for this case. Why not allow S[a/x, b/x]? Section 14 Instantiation ------------------------ Section 15 Semantic transformation ---------------------------------- 31) [minor] In clause 15.2.4.1, a note explaining that bowtie is used as a stroke (and perhaps a note in the lexis about it) would help the reader. 32) [major] Rule 15.2.5.8 is incorrect. For example, given S == [x,x': \num | x < x'], in working out "S \semi S", we have e_3 and e_4 both empty, and transformed expression is incorrect. A similar problem afflicts 15.2.5.9 Section 16 Semantic relations ----------------------------- 33) [major] Clause 16.2.1.1 does not work in the case of sections presented out of order. While Clause 13.2.1.1 shows that there is a permutation giving definition before use, at no stage is there a transformation that reorders the sections according to that permutation. 34) [major] Clause 16.2.1.1 suggests that a specification must explicitly include the Toolkit if it is used. This is unlike the Prelude, which is implicitly included. The toolkit should be available for use even if not explicitly included in a specification. This will certainly be needed for specifications derived from sequences of paragraphs. e.g., "a == \emptyset[\num]" is a legal specification according to tradition, but not according to this definition. 35) [minor] Rule 16.2.2.1 should perhaps add a constraint that the various models M_i are compatible (e.g., M_0 \simeq M_1 \land \dots), so that the union is always a function. 36) [minor] In the equation of Clause 16.2.3.3, the "\dom u" appearing in the last line could more simply be "W", as u is a function from W to W. 37) [minor] 16.2.3.4 There are two different interpretations of the validity of a conjecture. e.g., in the specification AX a: \Arithmos END |=? a = 0 END AX | a = 0 END the given conjecture is valid for the specification as a whole, but is NOT valid in the place it occurs (that is, at that point in the specification we do not yet know that a is 0). Perhaps the standard should clarify which of these two interpretations is intended. We believe the second interpretation is more useful, as it allows a conjecture to assert the consistency of the following paragraph. That is, the conjecture in S == \emptyset |=? S \neq \emptyset AX a: S END is always valid if conjectures are relative to the entire specification, but not if conjectures are relative to the partial specification up to where they occur. 38) [major] In the equation in Clause 16.2.5.14, the final t_1 should be t_2. 39) [major] In the equation in Clause 16.2.6.6, $M \oplus \{ i_1 \mapsto w_1, \dots \}$ should be $M \oplus \{ (decor \spades i_1) \mapsto w_1, \dots \}$ Annex A ------- 40) [minor] A.2.5 Can ".." be used instead of \upto? Is "{\cat}/" equivalent to "\dcat"? These equivalences seem to be implied by the specification of this Annex, yet are not likely to be supported by existing tools. 41) [minor] In A.2.6.3,, "Predicate" is misspelled. 42) [major] A.2.6.5 "&" is a special character in TeX, and cannot be used to join free type definitions. "\&" could be used instead. 43) [major] A.2.6.6 cannot be correct. An ENDCHAR is needed at the end of a paragraph. Many existing tools allow paragraphs in a zed box to be separated by "\\" or "\also", which here represents NLCHAR. According to 6.4.4.4, NLCHAR and ENDCHAR are different. 44) [major] Clause A.2.8 What are the scope rules regarding these introductions? Is a ZChar association active only within its section, or it is global? Does its effect occur only for the text following it, or for the entire text of a section (or specification)? Is redeclaration allowed? Is it legal to write \foo == 1 %%Zstring \foo {bar} \foo == 2 and if so, it this equivalent to foo == 1 bar == 2, or is it illegal to introduce an association for a command that has already been used? If the above IS legal, does the reordering of sections affect the scope? If ZChar and ZString declarations are scoped within sections, the processing required to determine section boundaries can be nontrivial. Consider \begin{zed} \zsection A parents B \zsection C parents D \foo B a == 1 \zsection D b == 1 %%ZString{\foo}{\zsection} \end{zed} Probably it is best to disallow "\zsection" from appearing in a ZString. Is something like %%ZString \foo {%%ZString \bar {%%Zstring}} allowed? 45) [minor] Clause A.3.2.2 In Example 2, the final line should probably read name' = name %u { n? } rather than name ' = name %u n? Annex B ------- 46) [minor] B.7.12 Does not specify that (1,0) is not in the domain of _ div _ or _ mod _. At a minimum, it should guarantee that (1,0) is not in the domain of (_ dom _) \rres \num. No matter how the numbers are extended, division by 0 should not result in an integer. 47) [minor] B.8.2 Spivey allows negative iteration; why be different? 48) [minor] B.8.6 Is "items" useful in the absence of bags? Why not eliminate it? Annex D ------- 49) [minor] In D.5.4, the semantic relation should be just the empty set, as the given paragraph is unsatisfiable for X = {} (and thus there are no functions giving a suitable meaning for i). Perhaps a different example should be chosen to illustrate looseness. GENAX [X] i: P X END would work. PART B ------ Comments on the mechanics and wording of the Document, with suggested clarifying wording. All but one of the items in this section are minor matters: 1) introduction page viii bullet 3 "checks on a specification to be performed automatically." 2) 4.1 definition of = "defines a non-terminal on the left in terms of the syntax on the right" 3) 4.1 meta identifier character section is surrounded by question marks. 4) 4.1 Some of the characters in this table are subsequently used without being explained, notably the bullet @. It may be that in the several places we have noted a term or symbol being used without explanation, an expert reader would not stumble. However, an IS should be able to stand on its own. 5) 4.2.2, table 2 needs a comma after the first "e" 6) 4.2.3.3 table 4 uses @ (bullet) for the first time without ever saying what it is‹part of the syntax, separating the declaration part of a quantification from the predicate part. Also, there should be horizontal separators to keep the explanations apart. 7) 4.2.3.4 The last word on the first line should be "falsity" not "falsehood". 8) 4.2.3.4 Table 6 has an unclear explanation 9) 4.2.4.1 last phrase is ambiguous, should it be "nature, and without abstracting meaning from their..." ?? 10) 4.2.4.3 We think this should be "then shows how to...pairing, of union, and of subset or separation." to properly balance up the sentence 11) 4.2.4.3 Table 8, line 1 should be "x %e (/) is always false" The word "comprehension" should be in the table of definitions and the index. 12) 4.2.4.4 "the existence of a powerset (the set of all subsets of a set.)" Otherwise the word "this" at the end of the next sentence is ambiguous. 13) 4.2.5.2 The lambda symbol is not in fact explained; rather, some examples using it are provided. No explanation is given of the symbol. 14) 4.2.5.4 sentence 2. "partial function" and "function" do not normally mean the same thing, so some further explanation seems to be in order. 15) 4.2.5.5 "..x represents the ..." Also, we are not sure about that last sentence, as normally one would not say that a function could produce non-unique values. 16) 4.3 Tables 18 and 19 are very interesting, but are presented with no explanation of some of the terms in table 18 (some MAY be self-explanatory) and none at all of what the tokens in table 19 are. 17) 4.4 below table 21, throughout this section, and in other places, the symbol |- is used, but earlier in the document it was stated (and this is consistent with the lists of valid symbols in two places) that a similar-appearing symbol has been replaced by the symbol |=. The symbol |- here is said to be "traditional" but is never defined. There is plenty of room for confusion here. "|-" used to be used in Z itself, to mark a conjecture in a specification. That has been changed to "|=?". "|-"is also used in the standard to describe the type checking rules. This latter use is not exactly "traditional", but is common in describing type systems by deduction rules. To compound the confusion, "|-" has a standard meaning in logic, and even though type theorists use deductive systems, they do not use "|-" with this standard meaning! Some explanation of how it is used would be useful. 18) 4.5 note 2. The heart and the spade are used here for the first time. Perhaps they should be in 4.3 with the bowtie stroke, along with an explanation. 19) 5.2.1 last line replace "which" with "that" 20) 5.2.5 in the two examples, the meaning of the bars has not been previously stated in the document. We note that it is explained later, in section 8.5, and perhaps a cross-reference could be placed here. 21) 6.2 SPACE is not defined. This may seem trivial, but does space = whitespace? i.e. is only one character in view, or are others possible? This becomes rather important in 7.3 22) 6.4.3.2 the last three words of the first line are redundant 23) 6.4.5 %E "there exists" 24) 7.2 "NUMERAL" not "NUMBER" (and elsewhere) 25) 8.3 "(and so that bind more strongly)" The last sentences of this paragraph are unclear. One could read them as referring to a table. 26) 13.2.3.4 line two of the paragraph "shall all be names of sets." 27) C.1 Introduction The word "following" is ambiguous. 28) C.3.2.2 paragraph1,line 4 As this section is said to be informative rather than normative, the word "shall" should not be used. (Check throughout such informative annexes for numerous such instances.) Or, perhaps the intention is that this annex summarize normative material, in which case "shall" is correct. Note that at the FDIS stage, this would be regarded by ISO as a major flaw. 29) D.8.3 The printing of Figure D.4 trespasses on the page footer, making both illegible. 30) D.9 para 3 "premiss" (spelling) _____________ end of Canada comments; beginning of Japan comments _____ ------------------------------------------------------------------------ ISO/IEC Vote on FCD 13568 Date of Circulation: 1999-09-01 Closing date for voting: 2000-01-04 Reference number: ISO/IEC JTC 1/SC22 N2982 ------------------------------------------------------------------------ P-members have an obligation to vote ------------------------------------------------------------------------ ISO/IEC JTC 1/SC22 Title: Programming languages, their environments and system software interfaces Secretariat: U.S.A. (ANSI) ------------------------------------------------------------------------ Please send this form, duly completed, to the secretariat indicated above. ------------------------------------------------------------------------ CD: FCD 13568 TITLE: Information technology - Programming languages - Z Specification Language ------------------------------------------------------------------------- Please put an "X" in the appropriate box(es) Approval of the draft: _____ as presented _____ with comments as given below (use separate page if necessary) _____ general _____ technical _____ editorial __X__ Disapproval of the draft for reasons below (use separate page as annex, if necessary) __X__ Acceptance of these reasons and appropriate changes in the text will change our vote to apoproval. _____ Abstention (for reasons below) ------------------------------------------------------------------------- P-member voting Date: Signature (if mailed) _________________________________________________________________________ Japan's Comments on ISO/IEC FCD 13568 (22 N2982) Title: Information technology - Programming languages - Z Specification Language The National Body of Japan disapproves ISO/IEC FCD 13568 for the reasons below. If the "General" and "Technical Major" comments are satisfactorily resolved, it will change its vote to approval. Item Number: JP1 Qualifier: General Reference: All Rationale: The term "Unicode" is used in the current FCD, but "ISO/IEC 10646-1" should be used in normative parts of ISO documents because the right reference for characters in ISO is ISO/IEC 10646-1: 1993, which is a correspondence in ISO to Unicode Standard. Proposed Action: The following actions shall be performed throughout the document: * "Unicode" as a standard shall be replaced with "ISO/IEC 10646-1". * "Unicode characters" shall be replaced with "the characters which are registered in ISO/IEC 10646-1 with its Amendments". * "16-bit Unicode" shall be replaced with "UCS-2". * "Unicode representation" shall be replaced with "the representation defined in ISO/IEC 10646-1 with its Amendments". * "Unicode value" shall not be used. See JP2. If necessary, "The character name defined in ISO/IEC 10646-1 with its Amendments" shall be used. * "Unicode" in tables in 6.4 shall be replaced with "ISO/IEC 10646-1". See also JP2. Furthermore, the following actions shall be performed for NOTE1 in 6.4.1 which explains the status of the proposal of the undefined Unicode values to Unicode Consortium: * Refer to "Unicode Standard" as an informative reference in Bibliography, whose reference number is assumed to be [x] here because of the reference in the next item and JP2. * Add the following NOTE after "ISO/IEC 10646-1: 1993" in "2 Normative Reference": NOTE In this standard, a limited part of characters in BMP of ISO/IEC 10646-1, that is, only mathematical symbols, are necessary in order to specify the Z Notation. These symbols are the same as those in Unicode Standard [x]. In sections below, the term "Unicode", if it appears, is used only for this limited character repertoire and not for character encoding issues. Item Number: JP2 Qualifier: Technical Major Reference: 6.4 and related (sub)clauses Rationale: Some Z characters have no code value in ISO/IEC 10646-1. This implies that code values cannot be used for identification of the Z characters. References of undefined values of "Unicode" columns in tables in 6.4 are not admitted as an International Standard. Furthermore, the Unicode values only corresponds to those of UCS-2 in ISO/IEC 10646-1, in which other code values for UCS-4, UTF-8 and UTF-16 may be also used. Generally, other code values than those of ISO/IEC 10646-1 should be allowed because each national body standard may admit the use of the non-ISO/IEC 10646-1 characters and their encoding schemes, e.g., an original JIS (Japanese Industrial Standard) code is very popular in Japan. Characters' identification shall not rely on their specific code values. This may be resolved by using character names which are defined uniquely in ISO/IEC 10646-1 (and Unicode), and which are independent of code values. See also JP1 for the term "Unicode". Proposed Action: Replace the "Unicode" line in 6.4.1 with the following: ISO/IEC 10646-1: Character name which is defined in ISO/IEC 10646-1 for the Z character. This column is provided only if the character is registered in ISO/IEC 10646-1. Replace NOTE1 in 6.4.1 with the following: NOTE1 Not all Z characters are currently supported by ISO/IEC 10646-1. Therefore, "ISO/IEC 10646-1" columns in the following subclauses exist only if the character is registered in ISO/IEC 10646-1. The characters which are not registered in ISO/IEC 10646-1 and/or Unicode Standard [x] are included in the AMS/STIX mathematical character proposal for the next version of Unicode Standard, which is expected to be also proposed to ISO/IEC 10646-1. Replace "Unicode" with "ISO/IEC 10646-1" if definite values for Z characters exist, and delete "Unicode" columns if definite values don't exist. Code values for Unicode shall be replaced with the corresponding characters' names which are defined in ISO/IEC 10646-1 as follows: * U+0030 -----> DIGIT ZERO * .. -----> .. * U+0039 -----> DIGIT NINE * U+0041 -----> LATIN CAPITAL LETTER A * .. -----> .. * U+005A -----> LATIN CAPITAL LETTER Z * U+0061 -----> LATIN SMALL LETTER A * .. -----> .. * U+007A -----> LATIN SMALL LETTER Z * U+0394 -----> GREEK CAPTIAL LETTER DELTA * U+039E -----> GREEK CAPITAL LETTER XI * U+03B8 -----> GREEK SMALL LETTER THETA * U+03BB -----> GREEK SMALL LETTER LAMBDA * U+03BC -----> GREEK SMALL LETTER MU * U+0027 -----> APOSTROPHE * U+0021 -----> EXCLAMATION MARK * U+003F -----> QUESTION MARK * U+2197 -----> NORTH EAST ARROW * U+2199 -----> SOUTH WEST ARROW * U+2198 -----> SOUTH EAST ARROW * U+2196 -----> NORTH WEST ARROW * U+005F -----> LOW LINE * U+0028 -----> LEFT PARENTHESIS * U+0029 -----> RIGHT PARENTHESIS * U+005B -----> LEFT SQUARE BLACKET * U+005D -----> RIGHT SQUARE BLACKET * U+007B -----> LEFT CURLY BLACKET * U+007D -----> RIGHT CURLY BLACKET * U+300A -----> LEFT DOUBLE ANGLE BLACKET * U+300B -----> RIGHT DOUBLE ANGLE BLACKET * U+2577 -----> BOX DRAWINGS LIGHT DOWN * U+250C -----> BOX DRAWINGS LIGHT DOWN AND RIGHT * U+2550 -----> BOX DRAWINGS DOUBLE HORIZONTAL * U+2029 -----> PARAGRAPH SEPARATOR * U+2028 -----> LINE SEPARATOR * U+0020 -----> SPACE * U+007C -----> VERTICAL LINE * U+0026 -----> AMPERSAND * U+22A8 -----> TRUE * U+2227 -----> LOGICAL AND * U+2228 -----> LOGICAL OR * U+21D2 -----> RIGHTWARDS DOUBLE ARROW * U+21D4 -----> LEFT RIGHT DOUBLE ARROW * U+00AC -----> NOT SIGN * U+2200 -----> FOR ALL * U+2203 -----> THERE EXISTS * U+00D7 -----> MULTIPLICATION SIGN * U+002F -----> SOLIDUS * U+003D -----> EQUALS SIGN * U+2208 -----> ELEMENT OF * U+003A -----> COLON * U+003B -----> SEMICOLON * U+002C -----> COMMA * U+002E -----> FULL STOP * U+002B -----> PLUS SIGN * U+2194 -----> LEFT RIGHT ARROW * U+2192 -----> RIGHTWARDS ARROW * U+2260 -----> NOT EQUAL TO * U+2209 -----> NOT AN ELEMENT OF * U+2205 -----> EMPTY SET * U+2286 -----> SUBSET OF OR EQUAL TO * U+2282 -----> SUBSET OF * U+222A -----> UNION * U+2229 -----> INTERSECTION * U+005C -----> REVERSE SOLIDUS * U+2296 -----> CIRCLED MINUS * U+22C3 -----> N-ARY UNION * U+22C2 -----> N-ARY INTERSECTION * U+21A6 -----> RIGHTWARDS ARROW FROM BAR * U+2218 -----> RING OPERATION * U+25C1 -----> WHITE LEFT-POINTING TRIANGLE * U+25B7 -----> WHITE RIGHT-POINTING TRIANGLE * U+007E -----> TILDE * U+2295 -----> CIRCLED PLUS * U+21A3 -----> RIGHTWARDS ARROW WITH TAIL * U+21A0 -----> RIGHTWARDS TWO HEADED ARROW * U+002D -----> HYPHEN-MINUS * U+2212 -----> MINUS SIGN * U+2264 -----> LESS-THAN OR EQUAL TO * U+003C -----> LESS-THAN SIGN * U+2265 -----> GREATER-THAN OR EQUAL TO * U+003E -----> GREATER-THAN SIGN * U+0023 -----> NUMBER SIGN * U+2329 -----> LEFT-POINTING ANGLE BLACKET * U+232A -----> RIGHT-POINTING ANGLE BLACKET * U+21BF -----> UPWARDS HARPOON WITH BARB LEFTWARDS * U+21BE -----> UPWARDS HARPOON WITH BARB RIGHTWARDS Move the list of Unicode values to a new informative annex as an example of implementations of the Z characters by Unicode encoding scheme. E-mail mark-ups in Annex A may be added in tables of 6.4 if more definite identification is necessary. For the replacement of "Unicode" with "ISO/IEC 10646-1", see JP1. Item Number: JP3 Qualifier: Technical Major Reference: 4. and 9.2 Rationale: The metalanguage symbols which are not given in 4., such as '\langle', '\rangle' and '\cat', are used in 9.2. They shall be added in 4. Proposed Action: Add "Sequences" which includes '\langle', '\rangle' and '\cat' in the appropriate place of 4.2. Item Number: JP4 Qualifier: Technical Major Reference: Fig.1 in 5, and 5.3 Rationale: The term "kernel syntax" is used, but there is no definition of "kernel syntax" in the current FCD. Proposed Action: Either of the following alternatives shall be performed: * Replace the term "kernel syntax" with a phrase "a reduced subset of the annotated syntax". * Give the definition of "kernel syntax" in a new clause, which shall be placed between the current Clause 14 and the current Clause 15. Item Number: JP5 Qualifier: Technical Major Reference: 7.4.3, 8.2, 8.4, 11.2, B.3.6 and B.4.2 Rationale: It is improper that the powerset construction rule does not appear in the concrete syntax while it appears in the annotated syntax. The powerset constructor \power is one of the most fundamental type constructors in the Z notation. It should be treated as a keyword token and the powerset construction rule using it should be included in the definition of the concrete syntax. It seems that \power is treated as generic with the intention of re-using operator templates by decorating operators. However, it is only an operator template that can be re-used by decoration and the new definition (declaration of types, properties, etc.) of decorated operators must be done. Decoration of operators seems to be different from that of schemas, which might be confusing. To propagate the Z notation, the proper treatment of the constructor \power is more important than confusing decoration of operators. Proposed Action: The following actions shall be performed: * Add \power to symbolic keywords in 7.4.3 as follows: Math Token Spoken name ... ... ... \power \power powerset ... ... ... * Add the following powerset construction rule to the definition of the concrete syntax in 8.2 as follows: Expression ::= ... | \power , Expression (* powerset *) | ... * Delete the following notation on \power from the prelude in 11.2: generic 80 (\power _) The precedence of the prefix generic operator \power is 80. * Delete the following note on \power from 8.4: NOTE4 There is no production specifically for powerset. It is introduced as a generic operator in the prelude, as otherwise \power_1 in the mathematical toolkit could not be parsed. * Delete the following note on \power from B.3.6: NOTE1 The \power symbol is established as a generic operator by the prelude. * Give up the re-use of operator templates by decoration, and add the following operator templates to the mathematical toolkit: - In B.3.6 Non-empty subsets, generic 80 (\power_1 _) - In B.4.2 Non-empty finite subsets, generic 80 (\finset_1 _) Item Number: JP6 Qualifier: Technical Major Reference: 8.2 and B.8.10 Rationale: In the current FCD, relations/functions/generics can be declared to take arbitrary number of arguments using ",," token in declaring their corresponding operator templates. For example, in the Mathematical Toolkit, B.8.10, the Sequence Bracket is declared with the following template: function ( < ,, > ) Now consider the following use of this function "< ,, >": < 1, 2 > This is a phrase of the Expression class of the concrete syntax. According to the current concrete syntax defined in Clause 8, this Expression phrase is parsed at the concrete syntax level (by skipping several production steps) as: < is a token of the class L; 1, 2 is a phrase of the ExpressionList class but NEVER an Expression phrase; > is a token of the class SR. The important point is that the arugument-list "1, 2" for the arbitrary number of argument place (specified by ",," in the template) is NOT a phrase of the Expression class. "1,2" in this example is a phrase of ExpressionList. Moreover, there is no production rule for the Expression class of the current concrete syntax that Expression ::= ... | ExpressionList | ... Therefore, there is no way to use such argument-list passed to the place of arbitrary number of arguments (in this case, "1, 2") in, say, the predicate part of an axiomatic description describing the property of such operators like "< ,, >". Intuitively, such an argument-list may be considered as an Expression of the type "seq T" for some type T (in the above example, T is \nat). In fact, in B.8.10, the generic function "< ,, >" is defined to take an argument of the type "seq X". This fact reflects that this FCD implicitly adopts the above intuitive identification of phrases of the ExpressionList class and phrases of the Expression class with a "seq T" type. But there is no explicit description of this identification. In the current FCD, such formal identification is only done in the Annotated Syntax level by a syntactic transformation rule, 12.2.12. But this is only at the level of the Annotated Syntax and never at the Concrete Syntax level where users of Z describe their Z specifications. Formally speaking, a phrase of ExpressionList has no relevance with a phrase of Expression of a type "seq T". Therefore, this intuitive and implicit identification must be clearly stated in the normative part of the FCD. This is the first point. The second point is as follows. Moreover, in the FCD, it is possible to write a specification without importing (by specifying in "parents" part) the Mathematical Toolkit, especially without importing operations of sequences defined in B.8. Therefore, in such a specification, Z users can write a specification with an operator taking arbitrary number of arguments by ",," notation, but users cannot describe properties of such an operator because there is no way to handle such an argument-list. In order to handle such an argument-list, users must be able to use operators for sequences defined in the Mathematical Toolkit. This means that the current FCD provides only one side for such a kind of operators (taking arbitrary number of arguments); that is, it provides only the way to define them and does not provides the way to use them. This is a severe lack of balance in language definition. Proposed Action: Add the following sentence (or alike) in the Subclause 8.2: a phrase of the ExpressionList class as a list of arguments passed for the place of arbitrary number of arguments specified by ",," in an operator template shall be regarded as a phrase of the Expression having some appropriate sequence type. Move minimal staffs for defining and manipulating sequences provided in the Mathematical Toolkit (especially, B.8.7, B.8.10, B.8.3, B.6.7, B.6.1, B.4.1) to the Prelude, Clause 11 so that users can use those operators without importing the Mathematical Toolkit. Item Number: JP7 Qualifier: Technical Major Reference: Throughout 9.2 Rationale: It is necessary to distinguish parentheses "(" and ")" of the metalanguage from those of the object language, Z itself. In fact, "(" and ")" which appear in the right-hand side of the 2nd defining rule of mktuple are those of Z, and other "(" and ")" are of the metalanguage, but the difference is unclear. This unclearness may cause readers' confusion. Proposed Action: Replace "(" and ")" of the metalanguage with double brackets "[[" and "]]". Item Number: JP8 Qualifier: Technical Major Reference: 10.2 (the production rule of Type), 13.2.5.1 and other related parts Rationale: It is necessary to distinguish between variable types and metavariables over Type in order to prevent ambiguities/confusions caused by identifying them. Proposed Action: The following actions shall be performed: * Use $\tau$ only for metavariables over Type. * For variable types (phrases of Type), use $\alpha$, hence the production rule of Type shall be changed as follows: | $\alpha$-tok , { STROKE } (* variable type *) * Replace the following use of $\tau$ (usages of $\tau$ as variable types) with $\alpha$: - All uses of $\tau$ in subclauses of 12 (12.2.6.1, 12.2.10.3, etc.) since those $\tau$s represent introduction of fresh variable types. - In the "where" clause of the last rule (in p.62, after NOTE 2) of 13.2.5.1, + $\tau$ in the left-hand side shall be kept as it is (since it is a metavariable over Type) and + $\tau$s of $\tau_{1}$, ... , $\tau_{n}$ in the right-hand side shall be replaced with $\alpha$s. * In 13.2.5.3, add the following explanation for the case of the empty set extension: \Sigma |-^{\cal E} \{\} :: \power \alpha where \alpha is a fresh variable type which does not appear anywhere else Item Number: JP9 Qualifier: Technical Major Reference: throughout 12.2 Rationale: It is necessary to distinguish between phrases of the concrete syntax and those of the annotated syntax in order to prevent confusions caused by mixed syntax phrases. In fact, in the current transformation rule 12.2.3.3, "AX [ i == e ]" in its right-hand side is quite misleading. "AX", "[" and "]" belong to the annotated syntax, while "i == e" is still in the concrete syntax; hence this rule 12.2.3.3 is quite confusing for readers. Proposed Action: Enclose all phrases possibly belonging to the concrete syntax by double brackets "[[" and "]]". Item Number: JP10 Qualifier: Technical Major Reference: 13.1 and EXAMPLE 1 of 13.2.2.1 Rationale: The current definition of the notion of "well-typedness" is not clear. The notion of "well-typedness" implicitly assumes that the type of a paragraph must not contain any free (i.e., unbound) variable types. This notion, however, is very important, hence should be stated more clearly and more counter-examples should be given. Proposed Action: The following actions shall be performed: * Add the following sentence after the 3rd paragraph of 13.1: A paragraph is well-typed only if it does not contain any unbounded variable types, where "bounded" means that a type is assigned to a variable type by using rules of this Clause. * Add new counter-examples which should be rejected after EXAMPLE 1 of 13.2.2.1: EXAMPLE 2 | zero == \{\} | one == \{ \{\} \} | two == \{ \{\}, \{ \{\} \} \} | another\_two == \{ \{ \{\} \} \} All of these paragraphs are ill-typed, because each of them assigns a type containing an unbound variable type to the left-hand side name. Therefore they shall be rejected. Item Number: JP11 Qualifier: Technical Major Reference: 14.3 Rationale: Rules in subclause 14.3 are needed in the type inference process specified in Clause 13, hence the contents of this subclause 14.3 should be given in Clause 13. Proposed Action: Move the contents of subclause 14.3 to a very early part of Clause 13 (e.g., before the current 13.2). Item Number: JP12 Qualifier: Technical Major Reference: 15.2.5.8 and 15.2.5.9 Rationale: The right-hand side phrase of each of these rules is a mixture of metalanguage notations and the Z notation (th annotated syntax) itself. For example, each of these rules contains five "@"s. But the first 2 "@"s are of the metalanguage and the remaining 3 "@"s are of the annotated syntax. Therefore, the current presentation of these rules are very confusing and should be clarified. Proposed Action: Replace "let ... @" metanotations with "where" style metanotations used in Clause 13. Item Number: JP13 Qualifier: technical minor Reference: 13.2.1.1 Rationale: The prelude is a part of the normative definition, hence its signature should be explicitly given by the standard document itself so that readers can be relieved from calculating the signature of the prelude. Proposed Action: Give the signature, \Gamma_{0}, of the prelude explicitly as a note just after the rule of 13.2.1.1. Item Number: JP14 Qualifier: technical minor Reference: throughout 15.2 Rationale: According to Clause 5, all transformation rules in 15.2 shall generate phrases in the annotated syntax defined in Clause 10. But, for example, the resultant phrase of the transformation 15.2.3.1 are expressed as a phrase of the concrete syntax defined in Clause 8. Proposed Action: Replace all phrases of the concrete syntax by equivalent (in the sense of Clause 12) phrases of Annotated Syntax, and keep current phrases of the concrete syntax as informative notes if necessary. Item Number: JP15 Qualifier: technical minor Reference: 15.2.4.1, 15.2.5.6 and all other related parts Rationale: In applying the transformation rules in referenced subclauses, type information is not needed, while other rules in 15.2 needs type information. Therefore, the former should be separated from other rules of 15.2. Proposed Action: Create a new clause which should be placed between current Clause 12 and current Clause 13. Remove type inference rules in 13.2.4.6 and 13.2.5.19. Item Number: JP16 Qualifier: technical minor Reference: 16.2.2.1 Rationale: The prelude is a part of the normative definition, hence its denotation should be explicitly given by the standard document itself so that readers can be relieved from calculating the concrete denotation of the prelude. Proposed Action: Give the denotation of the prelude explicitly as a note just after the rule of 16.2.2.1 if it can be expressed as a reasonably finite semantic metanotation. Item Number: JP17 Qualifier: technical minor Reference: 16.2.5.3, 16.2.5.4, 16.2.5.5 and 16.2.5.6 Rationale: Semantics of several Z constructs are defined just by giving the semantics of the same constructs in the metalanguage level in these semantic relations. Therefore, semantics of those Z constructs are not specified at all; if a reader would misunderstand the semantics of those constructs, he/she would not be able to correct himself/herself even if he/she reads this Z definition. For example, the serious problems of the current 16.2.5.5 is the following: * If a reader misunderstood that "\power" denotes "the set of all finite subset of the set denoted by its argument expression", then the current 16.2.5.5 does not give the reader any chance to correct his misunderstanding. * The semantic equation of the current 16.2.5.5 can be consistently read under such misunderstanding; 16.2.5.5 cannot get rid of the danger of "wrong fixed-point" of meta-circular definitions. The same problems lie in semantic equations of other constructs (16.2.5.3, 16.2.5.4 and 16.2.5.6). Any language definition adopting the meta-circular technique should pay as many efforts as possible to prevent such danger leading "wrong fixed-point". Since we can use the semantic universe (W) in defining semantics of those constructs, NOT all of the set-theoretic constructs need to be primitive. Only some of them have to be regarded as truly primitive and other constructs can be expressed by these primitive constructs. In fact, the set extension construct, the powerset construct, and the tuple extension construct can be interpreted using the set comprehension construct in the semantic metalanguage with the aid of the semantic universe W. Here is a proposal of defining semantics of Z's powerset construct in terms of the set comprehension construct of the metalanguage: (* Replacement of the semantic equation of the current 16.2.5.5 *) [[ \power e ]]^{\cal} = \lambda M : Model @ \{ w : W | \forall x : w @ x \in [[ e ]]^{\cal E} M @ w \} This semantic equation has no danger of the "wrong fixed-point". Even if a reader initially had a misunderstanding about \power as explained above, he/she could correctly understand the *true* meaning of "\power" construct from this semantic equation. Proposed Action: Rewrite those semantic relations/equations using the Set Comprehension Notation as the defining metanotation. (An example is given in the Rationale.) Item Number: JP18 Qualifier: editorial Reference: Subclause 4.1, the 2nd paragraph after NOTE 1 and all other related parts. Rationale: Readability of Concrete Syntax in Clause 8 is not acceptable. Proposed Action: The following actions should be performed: * Change this paragraph as follows: A further change to ISO/IEC 14977:1996 is the use of multiple fonts; metalanguage characters are in Typewriter, non-terminals are in Roman, and comments are in Italic. * Apply this change of use of fonts to all the document. This change will affect Clauses 6, 7, 8 and 10. _____ end of Japan comments; beginning of USA comments ________________ The US National Body DISAPPROVES the ISO/IEC FCD 13568.2, Information technology - Programming languages - Z Specification language. with the following NB comments. The US will change its vote to approve when these general comments are addressed. General Comments Item: US 1 Location: throughout the document. Qualifier: G Rationale and Proposal: The essential US view of an International Standard for the Z Notation is that a Z user should find there a complete description of the constructs of the language and a clear and complete explanation of the meaning of each construct. The US position is that this FCD falls significantly short of that goal. Specifically, it appears to address the concerns of a tool builder much more than those of a Z user. The large number of stages between a construct a user would recognize and its meaning make the journey arduous. An additional difficulty is the extent to which certain constructs are eliminated completely as they are defined in terms of others. The US believes that in many cases an explanation of the construct in its own terms rather than by reduction would be clearer. Item: US2 Location: Cover Page. Qualifier: e Proposal: The US proposes that when copyright for the standard is conveyed to ISO, the authors should retain rights to the material in Annex B Mathematical toolkit and Annex D Tutorial so that this may be included in textbooks and other expositions of Z. Item: US3 Location: Foreword/Introduction Qualifier: e Rationale: The US recognizes that Spivey's book "The Z Notation: A Reference Manual" [14, 15] is a very widely used de facto standard for Z Proposal: The Foreword or the Introduction should state how the language defined in this FCD differs from the version in the Reference Manual. Item: US4 Location: 3 Terms and definitions Qualifier: g Rationale: The Reference Model for Open Distributed Processing (RM-ODP) is an established International Standard (IS10746) which contains general definitions of many of the concepts in Clause 3. In fact RM-ODP Part 4 uses Z to clarify some of its concepts. Proposal: The connections between these concepts and the RM-ODP terms be made explicit. The US will provide detailed suggestions at a later date. Item: US5 Location: 3.21, 3.4, and elsewhere Qualifier: g Rationale: The definition of theory in 3.21 differs strongly from established usage of "theory" as a set of sentences. See Joseph R. Schoenfield, Mathematical Logic, Addison-Wesley, 1967, pages 22 and 82, for example. Proposal: If the concept defined in 3.21 is needed in the document, find a different term for that concept. The definition of conservative extension in 3.4 also should be changed. See Schoenfield, page 41. Uses of the terms "theory" and "conservative extension" in the document should also be checked to see that they are consistent with the corrected definitions. Item: US6 Location: 4.1 Syntactic metalanguage Qualifier: e Proposal: Remove the "?" before and after the definition of Meta identifier character. Item: US7 Location: 4.2.3.1 Qualifier: g Proposal: The clause "and the theory in this International Standard is intended to be consistent" does not make much sense. Probably the entire sentence should be omitted. Item: US8 Location: Tables 23, 24, 25, and elsewhere Qualifier: g Rationale and Proposal: The symbol "Theory" defined in Table 23 and the corresponding symbol "T" defined in Table 24 are completely inappropriate for the concept defined. If the concept defined is the right concept, then the term "Theory" should be changed. The second entry in Table 24 and other occurrences in the document, for example in Table 25, should be changed as well. Item:US9 Location: 5.2.4 Qualifier: g Rationale and Proposal: The US proposes that a conforming mathematical toolkit may define fewer or more notions than the toolkit in Annex B. However, if a conforming toolkit uses a section name which is used in Annex B, the set of concepts defined in the section must be the same. Furthermore, whenever a conforming toolkit does define a notion which is defined in Annex B, the two (partial) specifications must have the same set of models. Item: US10 Location: 5.2.5 Qualifier: g Rationale: Given the statement in 5.2.2 NOTE 1, the definition in the first sentence of 5.2.5 seems to require a strongly conforming Z support tool to process Z specifications given in any of an indeterminate set of alternate mark-ups. This is too strong a requirement. Proposal: The US proposes instead a requirement to accept specifications in (at least one of) or (both of) the LaTeX and email mark-ups. A note can then say that a tool may optionally accept specifications in alternate mark-ups, including its own proprietary mark-up. Item: US11 Location: 5.2.5 Qualifier: g Rationale and Proposal: The US proposes that if a support tool does not have the mathematical toolkit in Annex B as its default, it must clearly document the default toolkit it does provide (or the fact that it provides none) as well as any optional toolkit sections. Item: US12 Location: 5.2.5 Qualifier: g Proposal: Give some explanation of the significance of EXAMPLE 2 and EXAMPLE 3. If they are intended as examples of incomprehensible Z which is, nevertheless, technically correct, then say so. If they are intended to illustrate some other point, then explain it in English. Item: US13 Location: 6 Qualifier: g Proposal: In 6.2 and in each of the other formal grammars, the US proposes that the productions should be numbered. Item: US14 Location: 6.4.4.3 Qualifier: e Proposal: add "curly bracket" as an alternate to "brace". Item: US15 Location: 6.4.5 Qualifier: e Proposal: at a minimum add "back slash" as an alternate to "hide". It might be better to drop the name "hide". Item: US16 Location: 6.4.6 Qualifier: e Proposal: use "tilde" as an alternate for or instead of "inverse". Item: US17 Location: Clauses 7 and 8 Qualifier: g Rationale and Proposal: Clause 7.4.4 seems to contain the first mention of user-defined operators. The US believes that the current rules in clause 7 Lexis and clause 8 Concrete syntax are not sufficient to ensure proper parsing of expressions involving user-defined operators. A more detailed description of the problem and a possible solution will be provided at a later date. Item: US18 Location: 9 Characterisation rules Qualifier: e Proposal: For clarity, make the restrictions on n explicit by adding the following annotations: 1st rule for charac: ", where n >= 1" 2nd rule for charac: ", where n >= 1" 4th rule for charac: ", where n >= 1" 2nd rule for mktuple: ", where n >= 2" Item: US19 Location: 10.2 Qualifier: e Proposal: as in 8.2, change "(* free type *)" to "(* free types *)". Item: US20 Location: 11.2 Qualifier: e Proposal: in the paragraph immediately before NOTE 1, change "result disjoint from 0." to "result different from 0." Item: US21 Location: 12.1 Qualifier: e Proposal: In the first sentence of the third paragraph of 12.1, change "given for only" to "given only for". Item: US22 Location: throughout the document Qualifier: g Rationale and Proposal: The US proposes that, wherever possible, the language of the standard should be made clearer and more specific. Our intent is small editorial changes as illustrated in the next three specific proposals. Item: US23 Location: 12.2.5.3 Qualifier: g Proposal: change the last sentence to "It is semantically equivalent to the schema conjunction shown above." Item: US24 Location: 12.2.5.4 Qualifier: g Proposal: change the last sentence to "It is semantically equivalent to the schema disjunction shown above." Item: US25 Location: 12.2.5.5 Qualifier: g Proposal: change the last sentence to "It is semantically equivalent to the schema negation shown above." Item: US26 Location: 12.2.10.2 Qualifier: e Proposal: the right hand side of each of the transformation rules needs a space after the epsilon. Item: US27 Location: 12.2.10.3 Qualifier: e Proposal: the right hand side of each of the last two transformation rules needs a space after the epsilon. Item: US28 Location: 12.2.11.1 Qualifier: g Rationale and Proposal: the fourth transformation rule appears to have no effect. Delete it. 16 Semantic relations Item: US29 Location: 16.2.1.1 and 16.2.2.1 Qualifier: g Rationale and Proposal: "theories" is an inappropriate term to use here. Replace the term. Item: US30 Location: 16.2.2.1 Qualifier: g Rationale and Proposal: it is sensible to give a description in the form of an equation of the meaning of the simplest specification, the one containing only the section prelude. In addition, there should be a clear and complete description, in a form understandable by an ordinary Z user, of the meaning of this specification. Item: US31 Location: A.2.5 Qualifier: g Rationale: The first paragraph in A.2.5 assumes that support for the standard mathematical toolkit is all or nothing. This need not be the case. Proposal: The US proposes replacing the second sentence in A.2.5 with the following: "If any of the concepts in the standard toolkit are supported, the representation given here shall be used. Furthermore, if any of these notations is used, it shall represent the concept with the same set of models as the standard concept." Item: US32 Location: A.2.9 Qualifier: e Proposal: the second example in EXAMPLE 1 needs a space immediately before the final '. Item: US33 Location: A.3.4 Qualifier: g Proposal: replace the second sentence as in A.2.5. Item: US34 Location: D.4.3 and D.6.3 Qualifier: g Proposal: explain the notation used for the entries in Figure D.2 and Figure D.3, particularly the leading symbol which appears as an 8. ________________ end of SC22 N3048 ___________________________________