CASL V1.0 - Comments

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

Dear All,

Below some comments on V1.0. Most of them are typos.
A few may need some discussion.

Best regards,
Michel

                Comments on V1.0

page x (Contributors) Frédéric is mispelled Frédèric twice
page xii par. "Page 17": clsoe -> close, let is -> let it
page xiii par. "Page 55": extra `

page 3: I agree with Don that we should keep TF and PF disjoint ...
page 9: space is missing (twice) after bold keyword sorts (end of
2.1.1.1)
page 10, end of "Operation Types": `?S' should be `?s'
   WITH or WITHOUT a space between ? and s ???
Bottom of page 11: f:?s = T
   WITH or WITHOUT a space between ? and s ???
page 18, last par, 2nd line: Vns -->> Vn:s
page 20 and 21, 2.3.3.1: extra space in ` true'and ` false' (twice)
page 25: whould -> would

page 42, par 6.2.1:
  I find the concrete syntax (given SP"1,...,SP"m) a bit akward.
  I really do not like this given in parenthesis, as if it was not as
  important as the rest.
  I understand that () are needed to avoid potential syntactic
ambiguity, but
  I would much prefer 
    spec SN [Sp1]...[SPn] given SP"1,...,SP"m =
  even if this may seem to be contrary to linear visibility.
  This should have been discussed already, but I am afraided I missed
the
  point then.

page 58, 8.3.1.3: In the Meth. Note on arch specs, we have tentatively
used
a different and, say archand, displayed as \oplus, to emphasize the
different behaviour w.r.t. the and of struct. specs. Should we forget
this?
My suggestion would be archand for the input syntax, and $\oplus$ for
the
display syntax.

page 64: only to the the -> extra the

page 65, Bibliography: perhaps add the Meth note on arch spec there ?

page 54 vs C-6: I am not sure you use the same concrete syntax for
given.
  Page 54 given is used without ()
  Page C-6 () seem necessary.
  Of course I would prefer a version without (), perhaps restricting if
  necessary to only one UNIT-TERM (which can be an "archand" of
UNIT-TERMS)

PS: W.r.t. the discussion on compound ids. It has been advocated long
ago
in some notes by, on the one hand, Hubert, and on the other hand,
Andrzej
and myself, that it is much better to avoid any interaction between
compound ids and morphisms. Similarly (as more recently decided) for
compound ids and subsorting relations.
The only "exception" is for instantiation. In that case, special care is
given to the compound ids of the instantiated generic spec, and the
(extended) fitting morphism is composed with an appropriate renaming
which
will renames compound ids as appropriate. This special treatment doesn't
prevent to explain instantiation by means of union and renamings, it
just
requires a careful explanation of the renamings involved.

Michel