[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Minutes of Berlin meeting
[BKB: I share Andrzejs thoughts and conclusions below]
Dear All,
Following Bernd's call for comments, let me address perhaps the most
considerable change to CASL design proposed in Berlin, namely:
(viii) (no) sharing analysis in architectural specifications
(see my minutes of the semantics/language design groups meeting with
Bernd's comments sent to cofi-language on 13 April).
Having written the minutes and relatively not-quite-conclusive
conclusions on this point, and spending a while thinking about the
problem again, let me vote (with the majority of people present in
Berlin, with my abstention then) for the change of the design
following the possibility (**) in the minutes:
(**) Another possibility is to resign any sharing analysis in
the static semantics, and impose a corresponding condition to
ensure that the required amalgamations are well-defined within
the model semantics, thus turning it into a semantic
requirement (with a similar status as for instance
verification conditions occurring in the instantiation of
parametric specifications or in view definitions). Of course,
tool support would be expected to perform some (at least
static) sharing analysis and help to discharge the proof
obligation involved in most typical cases.
What we gain:
a) considerable simplification of the semantics of architectural
specifications --- as far as i can foresee now, it should become at
least as readable as other parts of the semantics, thus supporting
better explanation of architectural specifications :-)
b) institution-independence of the semantics of architectural
specifications.
c) no ad hoc conditions: static semantics as it is now, and as it has
to be in general, is to some extent arbitrary in deciding whether
or not a specification is well-formed. This is inherited from the
static analysis of sharing between components, which is
semantically incomplete -- a price to pay for decidability, of
course. However, in the case of CASL structures involving subsorts,
this incompleteness becomes somehow inherent --- we have no good
sharing analysis with decidable well-formedness conditions that
would be satisfactory from the semantic (and practical, I think)
point of view. With the change proposed, the condition becomes by
definition just the right one to ensure semantic
well-formedness. Formally it will have a similar status as
well-formedness of instantiations of generics, where the fitting
morphisms must be shown to be a specification morphism.
d) a related point is that now support tools can go as far as their
developer is able to into employing (at least) static analysis
means to show that semantically things are okay from the point of
view of amalgamability etc.
What we loose:
e) a close link from the CASL unit term language to the module system
of SML. There will be no easy way to introduce "generative"
character to CASL parametric units now. So far it was ensured by
the sharing analysis; after the change, this will be gone. I can
see no easy way to introduce generativity of just type system
without affecting other semantic aspects of the unit terms.
I think that one way or another this issue is a topic for serious
further study, as one aspect of the general problem of linking CASL
specifications with programming languages, and the final stage of
software development using CASL when a move to a programming
language is made.
f) potential decidability of this aspect of well-formedness of
unit-terms (and architectural specifications) in the cases where it
was possible (e.g., when no subsorts are present).
As far as I can see, both (e) and (f) can be removed to some extent by
some good tool support. I presume that any static analysis would
involve then a decent share (sic!) of sharing analysis, sufficient to
ensure that the semantic condition concerning amalgamability of units
is discharged in all typical cases when no subsorts are present, and
in many typical cases when there are subsorts around. Of course,
according to the semantics, the "warning" from such a tool that things
have not been shown correct is not a sign of an ultimate failure, but
only a very serious warning to the user that non-trivial proof is
necessary, and even if such a proof is performed successfully,
transforming unit terms involved to module facilities of a programming
language would still require nontrivial work.
Let me also add that this concerns a relatively little known corner of
CASL design, which is another excuse for me for proposing this change
now.
==============================================================================
PROPOSAL:
=========
I. Changes to the summary:
- In 8.3.1, 2nd paragraph: replace "For units, static semantics
requires that enough sharing is ensured so that the
constructs..."
by something like:
For units, enough sharing is required so that the constructs...
- In 8.3.1, replace 3rd paragraph
"Any sharing of symbols in a unit term must be supported by a
sharing of symbols in a common unit. (In the presence of
subsorts, the notion of sharing here is related to the
overloading relation.)"
by something like:
The sharing between symbols is understood here semantically: we
require that the same symbols coincide semantically. However, it
is expected that CASL tools would perform some static sharing
analysis by checking whether the symbols required to share in
fact originate from the same symbol in some unit declaration or
definition. This should be sufficient to discharge sharing
verification conditions implicit in the above semantic
requirement in most typical cases (in particular, when no
subsorting constructs are involved --- in the presence of
subsorts, the notion of sharing is related to the overloading
relation and involves implicit subsort embedings, which makes
compatibility of models much more complex).
- In 8.3.1.1, last paragraph: replace
"Any symbols that happen to be shared by the renaming must be
checked to originate from shared symbols in some unit."
by something like:
"Any symbols that happen to be glued together by the renaming
must share."
- In 8.3.1.5: remove " (by checking that shared symbols originate
from the same unit declaration)".
And using this opportunity, the notion of compatible models should be
explained correctly:
- In Ch. 7, one paragraph before the end, replace "Let us call such
arguments \emphindex{compatible}." by something like:
In the absence of subsorts, this is sufficient to allow one to
unambiguously \emph{amalgamate} arguments into a single model
over the union of argument signatures. When subsorts are present,
extra conditions to ensure that implicit subsort embedings can
be defined unambiguously in such an amalgamated model may be
necessary. Let us call arguments satisfying such a requirement
\emphindex{compatible}.
-------------------------------------------------------------------
II. Changes to the semantics (concerns the semantics task group):
- remove the sharing analysis from the semantics: tagging maps
disappear, sharing conditions disappear from many rules. This
will affect essentially entire static semantics of architectural
specifications.
- in place of sharing conditions, add to the model semantics of
unit terms the requirement that all values of components units
possible in the current unit context can be amalgamated (and the
same for unit translation). This will affect the rules for: unit
imports, amalgamation, translation and instantiation.
- add as an appendix a special "sharing-analysis semantics" which
would describe a desirable static sharing analysis procedure to
discharge the semantic conditions introduced above. This is
unlikely to be decidable in general when subsorting is involved,
but should be taken as obligatory for the static analysis tools
at least in the part concerning the sharing of sorts.
==============================================================================