[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
CASL - V 0.95
[I've removed comments about typos, also some comments that were
essentially making the same points as in the message sent by Andrzej
to cofi-language on Wed, 4 Dec 1996 17:14:47 +0100 (MET) --PDM]
Modular specifications (throughout the document): I am strongly against the
use of "modular" here, I am afraid this terminology is very
misleading. Besides unwanted confusions with the meaning of "modular" in
existing specification languages (e.g. in PLUSS modular specifications
correspond to architectural specs in CASL), from a more general point of
view I think that "module = structure + `autonomy'". Here the pieces of a
modular specification have no meaning, only the specification as a whole
has
[That is not consistent with my understanding of "semantics"!
Even the part that is used to extend some other specs should have a
perfectly well-defined meaning, also model-theoretically. --PDM]
(and it is a class of algebras without any structure, in contrast with
architectural specifications). Hence I would use as before "structured
specifications", where here structured has the same meaning as in
"structured programming": what we structure is the text of the
specification. As a last point, would you like to see my old note on
"structuring concepts" be renamed into a note on "modularity concepts" ?
This would clearly be totally misleading !
At least such a drastic change should have been discussed and approved in
Edinburgh...
[There seems to be considerable divergence of views on this topic.
Rather than wasting energy on it, let's revert to "structuring", even
though (in Edinburgh) several participants expressed dissatisfaction
with its connotations. I personally think that "modular" would be
fine, and Bernd liked it too, when I showed him a draft of v0.95.
The idea of using "modular" hadn't occurred to me until then, so it
was not possible to approve it in Edinbugh... --PDM]
p. v: WG 14.3 is now WG 1.3 ???
[It will become so, I believe, some time in 1997. Or perhaps it has
already? --PDM]
Study notes (pointers to): A new naming scheme is needed urgently if at all
possible to use it in the final final version ...
[Agreed. I'll propose one soon. --PDM]
[MB-2]: I am still willing to update my note on generic specifications in
order people can access a document consistent with the CASL Summary. By
this I mean to update my note to take into account decisions made in
Edinburgh. When I will be able to do this is unclear, perhaps before
Christmas ? Please announce a new forthcoming version.
[Thanks, that will be very helpful. --PDM]
p.3, 1.3, "explicitly-sorted term": please explain (in a footnote) that
this concept, which is obviously not needed at all in the absence of
subsorts, is nevertheless introduced here for consistency reasons.
[It is needed (or at least used) for determining well-formedness of
terms and formulae, even in the absence of subsorts! --PDM]
Sentences are ... the usual closed ....:
As far as I remember, we have decided in Edinburgh to allow formulas with
free variables (which should however have been declared in a corresponding
VAR-DECL). Whether we need also formulas with free variables at the level
of the institution is perhaps less clear, but why not ??? With the
assumptions that carriers are non empty and the usual satisfaction of
formulas with free variables...
[See Till's message earlier today on this topic. --PDM]
p.5, 2.1, l.4: several different types --> several different profiles
*** please do the same for all further occurrences of "types": FUN-TYPE is
more than the profile, profile is the terminology consistent with the one
used in 1.1 ***
[OK --PDM]
p.6, 2.3, last line (A well-formed axiom determines a sentence of the
underlying basic specification):
Here it must be made clear than we can write axioms with free variables
(with the usual interpretation), provided the free variables are declared
as explained in 2.2. The wording is OK if formulas with free variables are
there in the underlying institution, otherwise more explanations are
needed. But we have decided in Edinburgh that the usual style of, say,
equational specifications without explicit quantifiers was to be allowed in
CASL...
[See Till's message earlier today on this topic. --PDM]
A few lines above, "current declarations" (also in various other places):
the meaning is unclear, since the order of basic items is
irrelevant. Unfortunately, I am not able to provide a better wording...:-(
BTW, why have we decided that the order of basic-items is irrelevant ?
What is the rationale for this ??? Are we so sure this is the right
decision ??? Just makes tools more complex, semantics less clear, etc.
[Good question! We could require linear visibility, just as in
libraries - except perhaps in TYPE-DEFN-GROUP, where one has the usual
problem with mutually-revcursive types... --PDM]
p.7, last par of 2.3.1: I would suggest to remove this par, which I find
both unclear and irrelevant: the intuitive meaning of exists-uniquely is
clear, this quantifier may be defined in the underlying institution, so...
p. 8, about well-sortedness of applications (of predicate symbols, of
function symbols):
* ...when there is a declaration of a PRED-NAME (with the specified
PRED-TYPE, if any) such that...
* ...when there is a declaration of a FUN-NAME (with the specified
FUN-TYPE, if any) such that...
I am worried by the plural for "expansions": in the absence of subsorts,
there should be only one expansion ??? otherwise it is an error ???
(cf. also "those" line -2).
[A term may have several expansions, and the atomic formula in which
it occurs may insist on one of them, making the formula well-formed.
Please consult the study note on subsorting [MC++-1] for more details.
--PDM]
W.r.t. VAR in TERM, I believe it expands to the fully-qualified expansion
of the variable (the same as for a constant ?).
[Right. --PDM]
p. 9, 2.4: For the sort-generation to be well-formed, we must require also
that the result sorts of the FUN-SYMB are in SORT+ (otherwise it is an
error).
p.9, 2.5, intended interpretation: I am afraid I still find "freely
generated, persistent extension" quite unclear. Somehow type definition
groups are to be used as if they were basic items, although semantically
they are closer to basic specs ? How to explain this clearly ? How to
explain clearly that whatever the context where a type definition group
occurs, the semantics of this type definition group is the same (provided
it is well-formed) ?
[As I mentioned when forwarding Andrzej's message last Wednesday:
My personal view has always been that a TYPE-DEFN-GROUP (with or
without AXIOMS) is best regarded as a SPEC, not a BASIC-ITEM...
A compromise might be to allow a single TYPE-DEFN as a BASIC-ITEM, but
take a TYPE-DEFN-GROUP as a SPEC? Then (perhaps) a TYPE-DEFN in such
a context really would correspond to some declarations, some
disjointness axioms, and a sort-generation constraint? Clearly, one
wants to be able to abbreviate enumerations and sort unions as
BASIC-ITEMs. --PDM]
p.24, par -2: what is important is that the LIBRARY is linearizable.
I think that one day we will need to be able to introduce in a LIBRARY named
specifications where all named subcomponents are *not yet* defined. In that
case, of course, not much can be said about such a named specification, it
is needed to wait for the named subcomponents to be actually introduced
themselves in the LIBRARY. But the user needs to be able to define the
various pieces in the order that best suits him, not necessarily in a
bottom-up way. Or is this a tool issue ?
[A not-yet-defined component should perhaps correspond to a
place-holder of the right syntactic category; this would be easy to
add in a systematic way to the abstract syntax. But I don't see the
need (or possibility) to give semantics to incomplete specifications.
--PDM]
p. 32/33, Downloading: isn't this a TOOL issue ?
[The proposal is to provide a language construct to support the tools
that have to implement it. (Sub-languages may, of course, decide to
prohibit downloading.) --PDM]
Cheers,
Michel