Re: Comments on CASL v0.95 FINAL DRAFT

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

In rush, as too usual...

Best regards,

Andrzej
==============================================================================
Few immediate comments on the message from Till:
------------------------------------------------
Free variables, empty models, etc:

I do not like empty carriers either, but I dislike any manipulation
with free variables even more. (So, my "ideal" solution would be to
remove the non-empty carrier assumption and deal with closed sentences
as axioms only.) Given that people say that variable declarations as a
means to avoid some tedious quantification are a must, I'd rather have
the non-empty carriers assumption than arbitrary models and some rules
about closure wrt to variables that actually occur free in formulae,
or a separate and distinct treatment of free variables in the logic. I
would therefore also stick to the current text in the proposal, about
universal closure fo the axioms over the variables declared in the
given list of basic items. Just my opinion though...

> page 19, 6th para:
> ------------------
> The semantics of a SPEC-INST has to be defined not through a
> UNION, but through an EXTENSION, because a UNION cannot deal
> with PERSISTENT-SPECs and the freeness declarations
> wouldn't have the intended effect. 

My understanding was that both freenes and persistency requirements
are considered wrt the formal parameter specification. I think that
under some reasonable assumptions this comes close enough to "the
intended effect" (whatever it might be for this constructs). One way
or another, if we are to stick to the pushout-style semantics of
instantiation, I fear that trying to relate persistency and freeness
requirements to the actual parameter might force us into the smeantics
in a macro-expansion style here, closer to lambda-calculus style
parameterisation.

> Section 8, Architectural Constructs:
> ------------------------------------
> The former ARC-SPEC-REF, allowing to re-use arc specs within
> other arc specs, is missing now. Can the same effect be achieved
> by supplying for the UNIT-SPEC which is needed within a UNIT-DECL 
> just a SPEC-NAME which is bound to an ARCH-SPEC?
> 
> [If I followed the discussion in Edinburgh well enough, Andrzej's
> point was that such a reference would be misleading, not giving the
> intended effect.  ANDRZEJ: please clarify this!  --PDM]

I missed that change, sorry. I think it does make sense to refer to an
arch spec and use it as a normal spec. Yes, it would involve a
coercion from arch specs to structuring specs, given by computing the
class of possible units as described by the RESULT-TERM in the context
of the component units as declared in the arch spec. The point I was
making was that this might be different from the result spec of the
outermost unit applied in the RESULT-TERM -- and the point I was
trying to make was that in a sense this is right! If you want to use
this result spec, you can just use it. But you might also want to use
whatever comes out of an arch spec. I suspect this will not be very
often needed, but I can see not reason for exclusion either. 
==============================================================================
And small comments on some points from Michel:
----------------------------------------------

> 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).

maybe an error, maybe not :-) As usual, i would avoid introducing
semantically unnecessary context conditions.

> 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.

It is very true that allowing an arbitrary order between basic item
makes amny things more complicated. I do not think that we intend any
"mutual recursion" here, so it is also not really necessary. The only
argument for, as far as I recall was that it might be convenient to
write basic items in an arbitrary order... I personally would not mind
at all if this was changed back and the linear visibility was adopted
here as well.
==============================================================================