[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
More comments on 1.0
Dear all,
here are some more comments on CASL 1.0 draft.
Contents
--------
- Compound ids versus translation and reduction
- Institution independence
- Redeclaration
- Unit declarations
- Unit specifications
- Anonymous mixfix operator
- Editorial comments and typos
Greetings,
Till
Compound ids versus translation and reduction
---------------------------------------------
The 2nd last paragraph on page 49 reads:
Instantiation, however, does preserve subsorts: if in a generic
specification we have \Symb{Elem} declared as a subsort of
\Symb{Seq[Elem]}, where \Symb{Elem} is a parameter sort,
then in the result of instantiation of \Symb{Elem} by \Symb{Nat}, one
does get \Symb{Nat} automatically declared as a subsort of
\Symb{Seq[Nat]}. Similarly for translation and reduction.
The last sentence is new!
It suggests that not only instantiations of generics, but also
translations and reductions interact with compound ids.
An argument in favour of this would be that then the semantics
of institation can be really explained in terms of the
semantics of renaming, union and extension.
The main contra argument is that compound ids are specially
constructed for instantiations, in order to avoid name clashes
between two different instantiations of the same generic spec.
Is it methodologically useful to think of two different translations
of the same spec, which are then united? Surely, for example
when we want to get a generic spec with two similar but independent
parameters. But is a special treatment of compound ids useful in
this context?
Technically, it is not possible to introduce this interaction
only at the level of interaction with subsorting (i.e. in the above
quoted paragraph). Either, we have to introduce it from scratch (i.e.
translation and reduction interacts in the same way with compound
ids as instantiation, cf. the first paragraph on p. 49), or we
have to leave it out entirely.
Institution independence
------------------------
On p. 34, it is claimed that Parts II to IV of the summary
are orthogonal to Part I.
Now there are still some institution dependent parts in Part II, namely:
- At several places, the subsorting and/or the overloading relation
is mentioned. Not a big problem, since for institutions without that
stuff, just ignore it. And I am still considering to add an
overloading relation to the notion of institution (but have
come to no definite conclusion yet). For instantitiations of generics,
it would be safe to have both the pushout property and its
explanation in more concrete terms.
- "free types xxx" and "free {types xxx}" have the same semantics (p.
41)
This holds for the CASL institution, but may fail in extensions
(see L-10 about the HO extension). Probably this should be mentioned.
- Symbol lists and map. No problem, since this is collected in an own
section. However, outside this section, we should deal entirely
with qualified symbols, because the process of making a map of
unqualified symbols into a map of qualified symbols is very
institution-specific. I.e. "symbol" outside 6.4 (and 6.5)
always means "qualified symbol".
I therefore suggest to change the last paragraph in section 6.4.1:
"The list determines a set of qualified symbols, obtained
from the listed symbols by using qualification information
of a given signature..."
(Similarly for 6.4.2)
The signature is either the local environment signature
or the source signature of the signature morphism.
Redeclaration
-------------
p.8, l.11
"Verbatim repetition of the declaration of a symbol does not affect
the semantics." It should be mentioned that non-verbatim
redeclaration is allowed as well, i.e.
sort s
type s ::= ...
sort s = { ... }
This is allowed in the semantics, and I guess it would be
difficult to disallow it.
Unit declarations (8.1.1)
-----------------
A declaration
UN:US given UT
corresponds to implementing a generic unit function and applying
it once to UT. What is the argument type of this function? Just the
signature of UT?
Unit specifications (8.2)
-------------------
The last paragraph on p. 55 explains the use of named unit
specifications
for synonym definition. But this is only a very restricted form
of use - named UNIT-SPECs may also be used in unit declarations,
for example. The general use should be explained like:
" A UNIT-SPEC can also be just a SPEC-NAME, referring to a
unit specification definition in the global environment.
(Such a reference cannot, however, be distinguished context-freely
from a unit type without argument specifications. Therefore,
the abstract syntax contains no extra clause for this case.)"
Anonymous mixfix operator
-------------------------
I suggest to mention that the anonymous mixfix operator
might/will be reserved for application in the higher-order extension
(and therefore first-order specifications using it cannot
be used verbatimly in the higher-order extension).
Editorial comments and typos
----------------------------
p.2, line -9 to -6:
"The signature provided for a particular sentence in a specification..."
should be changed into
"The signature provided for a particular declaration or
sentence in a specification..."
since this is the full explaination of the local environment.
p.5, above 2nd itemize:
Implication may be regareded as primitive only in presence of
false - should this be mentioned?
p.5, l.-7 to -5:
Strong equations also may be derived from existential equations
using implication and conjunction:
t = u
is equivalent to
(t=e=t => t=e=u) /\ (u=e=u => t=e=u)
which is in positive conditional form!
p.7, last paragraph:
Logically, this paragraph would belong to section 2.3.4.
I guess that it was placed here in order to stress it as an
important general point. But I found that it rather abruptly
starts to talk about terms. What about
"While well-formedness of terms occurring in sentences of the
language ..."?
p.9, 2.1.1.1
Insert space between "sorts" and "s1...sn".
Insert a "sort" keyword before the last "sn".
p.10, 3rd line above Operation Attributes:
"?S" ==> "?s"
p.11, line -7
V1m1 looks a bit funny in my printout (but maybe the paper
was a bit dirty)
p. 17, 2.2.2 and 2.3
The last semicolon is optional in both cases.
p.18, l-10
"any values" => "some values"? (I don't know, just ask).
p.18, l-5
A colon is missing before the first s.
p.31, l.8
"make it well-formed" => "make them well-formed"
p.42, 6.2.1
Perhaps swap "imports" with "paramemters" because this order
is also used in the syntax?
p. 55, 3rd last paragraph
"US" => "USP"
Insert "an" at the end of the third line.
--------
Dear friends,
here are my final comments to CASL 1.0.
Contents
--------
- Library names
- Qualified ids in a symbol map
- Reserved tokens
- Examples
- Editorial comments/typos
Greetings,
Till
Library names
-------------
What is the relation between the LIB-NAME in a LIB-DEFN
and in a DOWNLOAD-ITEM? The latter specifies a directory
giving access to the library, while the former seem to be just
a name for documentation but irrelevant for the semantics.
If this is correct, the irrelevance for the semantics
should be explicitly stated.
Qualified ids in a symbol map
-----------------------------
I am still not sure which abstract syntax tree is associated
to
SP with c:s
I can see two ASTs. Both have the form
renaming SP (symb-map-items implicit (qual-id c t))
where t is either
total-op-type (sorts ()) s
or
pred-type (sorts s)
What do parser writers say (the Bremen parser is for basic
specs only, so far).
Reserved tokens
---------------
p. C-9
Is the reservation of {, }, [, and ] really necessary?
Probably it is necessary for LALR(1) parsers, but what
about ASF+SDF? It would be nice to have {__} and [__],
and {, }, [, and ] could be forbidden for parsers not
supporting mixfix.
Examples
--------
The N.B. paragraph on p. E-1 should be deleted or
reformulated. We should give examples that are as elegant
and concise as possible. Each feature of CASL can be
illustrated by such an example (otherwise, we have designed
a bad language).
The paragraph could say something like
The examples cannot show all features of CASL and all
styles of specifications supported by CASL, for this,
we refer to [some other forhtcoming document].
I would improve the examples and make them coherent, since
for the time when there are not other introductory documents
yet, these will be the most prominent examples of CASL
specifications, and therefore they should be as convincing
as possible.
I have the following suggestions:
E.4 SIG1 => SET1
E.5 SIG2 => SET2
E.7
This relies on Item <= List[Item].
E.10 should be adpated and placed before E.7, like
spec ELEM =
sort Elem
end
spec NON_EMPTY-LIST_OF[ELEM] =
free type List[Elem] ::= sort Elem | __ __(Elem;List[Elem])
ops first:List[Elem]->Elem
last:List[Elem]->?List[Elem]
vars e:Elem; l:List[Elem]
axioms first(e) = e
first(e l) = first l
not def tail(e)
tail(e l) = l
end
and then replace NAME by ELEM, Item by Elem and
add__to__ by __ __ in E.7.
E.8
Replace the parameter of LIST_WITH_ORDER by
PO with T |-> Elem
Examples for views and arch specs are still missing!
Editorial comments/typos
------------------------
p. C-1, 2nd item
Kolyang and I have written a parser, well-formedness
checker, and encoding into the Isabelle/HOL proof system,
but for basic specs only.
p. C-2, above C.2
"might" => "may"
p. C-7, 1st item
"rename", "require" => "with"
p. C-7/C-8
What is the precedence of TOKEN __ ... __ TOKEN ?
p. D-2, 2nd last paragraph
Why are semantic annotations not displayed?