Subject: CORRECTED SC22 N3048 - Vote Summary on FCD 13568: Z Specification Language (fwd)

From: William Rinehuls <[email-masked]>
Date: Mon, 10 Jan 2000 12:20:48 -0500 (EST)

Note:  The only change is to the references to the SC22 Working Group
responsible for handling the comments.  

__________________ 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:
WG19 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 WG19

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.

WG19 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 ___________________________________