[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Berlin meeting of the semantics task group
Dear Semanticists,
A one-session (1.5 h) meeting of the CoFI semantics task group took
place in Berlin on Sunday, April 2nd, within the CoFI workshop
accompanying ETAPS 2000. (Many thanks to the local organizers for
taking care of us throughout the workshop!)
Below are the minutes, composed by me on the basis of what I wrote
down and recall...
With best regards,
Andrzej Tarlecki
==============================================================================
Semantics Task Group meeting
Berlin, 2 April 2000.
Present (my apology for misspelling some names when copying from the
handwritten list): Andrzej Tarlecki (chair), Agnes Arnould, Serge
Auxieter, Hubert Baumeister, Michel Bidoit, Maura Cerioli, Ann
Haxthausen, Piotr Hoffman, Helene Kirchner, Bartek Klin, Bernd
Krieg-Brueckner, Pascale Le Gall, Till Mossakowski, Nikos Mylonakis,
Adumeur Nasreddia, Don Sannella.
1. Status of the semantics:
The current version of the semantics (v. 0.96, July 1999) was put at
the CD ROM material at FM'99 in Toulouse (and should be available from
the CoFI web page, of course). Some polishing and possible reworking
(see below) is required, but overall the semantics is largely
ready. One major exception is the semantics of architectural
specifications, which is likely to still undergo considerable changes,
and needs to be put in an institution-independent form.
(A meeting of the authors of the semantics took place in Berlin as
well, where we agreed to aim for June as a likely deadline for
completion of the semantics with all the necessary changes.)
Till Mossakowski briefly presented the current version of the
appropriate enrichment of the notion of institution ("institution with
symbols") that is used as a basis for the institution-independent
semantics of structured specifications. The need for further
modification of this notion to cover architectural specifications as
well depends on the crucial decision in 2.(viii) below.
2. Proposed changes for the semantics and language design:
This part of the meeting was agreed to be considered as a joint
meeting of the semantics and languages design task groups.
Although CASL design is fixed by now, and this stability is considered
to be very valuable, work on the semantics and on the examples
(e.g. basic datatypes) for CASL brings suggestions for various
modifications of CASL details. See below for the presentation of items
that have been discussed.
The overall recommendation is that the language design group should
take appropriate actions to introduce changes to the language design
and its summary description following the proposals.
3. Plans for further work:
Not much new was discussed here w.r.t. the minutes of the previous
meeting (Amsterdam, March 26th), except that the work on making the
semantics institution-independent progressed considerably.
==============================================================================
AD 2 (continued):
Proposed detailed modifications to the CASL language and its semantics:
-----------------------------------------------------------------------
(i) meta-foundations: axiom of choice.
The semantics of CASL is based, of course, on some semantic
universe, or more specifically on some assumed set-theoretic
foundations, never explicitly discussed so far. It was pointed
out (see e-mail from Till Mossakowski on 20.03.2000) that in
particular the axiom of choice may influence correctness of
some specifications (some verification conditions may depend
on it).
PROPOSAL: adopt axiom of choice, mention this at least in the
semantics (perhaps also in the summary).
(ii) default mechanisms for symbol maps
See Till Mossakowski's message on 20 December 2000: let
spec Sigma =
sort s
op f: s -> s
end
currently:
Sigma with s |-> t
is ill-formed, since the operation symbol "f: s -> s" (which
includes the profile) cannot be mapped identically to itself.
PROPOSAL: modify the language design so that the explicit
symbol maps are extended with identities on names (rather than
on symbols, as now).
In the above example, the induced signature morphism would map
"f: s -> s" to "f: t -> t" as expected.
This requires minor change in the summary.
(iii) symbol maps vs. local environments
See again Till Mossakowski's message on 20 December 2000:
currently, if a symbol is overloaded between local environment
and the specification being evaluated (the same name occurs
with one profile in a local environment and with another in
the current specification) then any attempt to rename the
symbol from the current specification by giving its name only
would yield an ill-formed specification (since this would also
imply an illegal attempt to rename symbol in a local
environment). One might consider a version of the semantics
which would hide any symbols from the local environment from
the domain of symbol maps.
PROPOSAL: no change! It seems advisable in such cases to
explicitly annotate the symbol from the current specification
with its profile, so that the confusion between symbols from
current specification and local environment is avoided
explicitly.
(iv) static denotations for structured specifications
Sasha Zamulin pointed out that the current static denotations
for structured specifications, which elaborate to signature
extensions, is perhaps unnaturally complicated: it seems that
the overall result signature should be sufficient here. The
authors of the semantics for the structured and architectural
specifications part of CASL confirm this. The situation may be
different for the semantics of basic specifications. One way
or another, this change will not affect the overall semantics
of the language constructs.
PROPOSAL: introduce this change to the semantics of structured
and architectural specifications. Don Sannella is to check
whether it is also possible/easy for the basic specifications:
either the change will be introduced throughout this part of
the semantics (and, consequently, for the subsorting part as
well), or just the overall "export" of the static analysis of
basic specifications will be adjusted to this style.
(v) signature unions
Currently the union of specifications containing an operation
symbol f:s->s and of f:s->?s (same name, profiles differ in
the "totality mark") is illegal. An alternative, more
consistent with the current possibilities offered by CASL
signature morphisms, would be to make such unions well-formed,
with "f:s->s" in the union signature. Consequently, this would
require changing the semantics of basic specifications to
allow for redeclaration of operation symbols with the same
names and profiles differing only in the "totality mark". The
overall idea here would be to treat symbols of total
operations as the corresponding symbols of partial operations
(same name, same arity, same result sort, but partial function
mark) with an extra build-in attribute (axiom) of totality.
Bernd Krieg-Brueckner raised objections on methodological
grounds. Moreover, as he pointed out later, it is relatively
easy to achieve a similar effect by simply translating the
specification with the partial function declaration by the
symbol map {f:s->?s |-> f:s->s}. This indeed seems easy
enough to make the benefits of the change less crucial.
PROPOSAL: no clear-cut recommendation whether this change
should be introduced has been reached.
The summary does not say anything explicitly about this, but
it seems that a natural reading would correspond to the
current semantics. If the decision to introduce a change is
taken then the summary has to state this explicitly; if the
decision is to stay with the current version then perhaps the
summary might be modified as well to make this clear.
(vi) extending view definitions
(see: Roggenbach, Mossakowski, Schroeder "Basic Datatypes in
CASL" v.0.4, pp. 68-69,
http://www.informatik.uni-bremen.de/~cofi/L-12_04.dvi)
It is possible in CASL now to name views, thus introducing
them into the global environment. However, only explicit view
definitions may be named in such a way, rather than arbitrary
"view expressions" present in other parts of the language (in
particular, view instantiations and view identifiers are not
permitted here). This seems to be an omission in the language
design.
PROPOSAL: table the extension of view definitions for the
first occasion when a major update of the language takes
place. The motivation is that the current changes should only
affect the summary in a relatively minor way; this change
would even require extension of the abstract syntax of CASL.
(vii) overlap between parameters and imports
(see: Roggenbach, Mossakowski, Schroeder "Basic Datatypes in
CASL" v.0.4, p. 69,
http://www.informatik.uni-bremen.de/~cofi/L-12_04.dvi)
There is a certain limitation on the import mechanism in CASL
structured specifications: only non-generic specifications can
be imported by a specification. As the result, if some part of
the parameter overlaps with import, it can only be
instantiated identically (since this is imposed on the entire
import part). It would be conceivable to allow non-trivial
instantiation of the parts of import that overlap with
explicit parameters. However, full consequences of such a
decision on the semantics of parameterised specifications with
imports were not clear to all present at the meeting.
Similar remarks apply to parametric unit specifications in
CASL architectural specifications.
PROPOSAL: table the issue for further study and possible
change in the future.
(viii) (no) sharing analysis in architectural specifications
There is a serious problem with the static semantics of
architectural specifications. It has been noted that the
institution of CASL does not have the amalgamation property:
there exist CASL models that coincide on the intersection of
their signatures and nevertheless they cannot be "amalgamated"
to a model over the union of their signatures (which would
extend each of the two models). This causes a lot of trouble
in the static semantics of architectural specifications. There
are some rather standard ways to perform a "sharing" analysis
there to determine which of the components of models
constructed must coincide ("share"). In view of the lack of
amalgamation property for CASL institution, this does not
easily indicate how to statically verify that amalgamations
involved in unit construction can be performed (the same
applies to translations and instantiation of generic units as
well). There is a rather complicated condition that ensures
this, as currently formulated in the semantics. However, it is
not clear whether this condition is decidable! (it is known
that a condition close to it is undecidable; it is also known
that the current condition could be made somewhat more
permissive at the expense of further complication of the
semantics; there seems to be no natural stronger condition
that would be known to be decidable and at the same time, in
the presence of subsorting, would allow all typical examples
to go through).
There are a number of possible ways out of this problem:
(*) One would be to leave things more or less as they are and
live with possibly undecidable static semantics. The
disadvantage is that now static analysis may well be
undecidable, and the semantics is rather complicated, without
any certainty that all what one might want to build is
allowed.
(**) 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.
The clear advantages of the latter possibility are a
considerable simplification of the semantics (which would then
be institution independent nearly for free, inheriting this
from the semantics of structured specifications), and a room
for arbitrarily elaborate sharing analysis (and perhaps
verification) to ensure well-formedness of unit expressions. A
disadvantage to be mentioned is that what typically is a
matter of static analysis in programming languages becomes
formally a verification issue in CASL. Moreover, it was a
static analysis that so far ensured that parametric units in
CASL are "generative", thus making them close and easy to
translate to SML modules. This direct link would be lost now.
(***) In principle, it would also be possible to mix the two
approaches, by imposing some "insufficient but expected"
condition for amalgamability in the static semantics
(e.g. performing the usual sharing analysis for sorts and
operations, but without considering subsort embedings), and
then adding an extra semantic check in the model
semantics. This however seems to pick disadvantages from both
possibilities while hiding their potential benefits.
PROPOSAL: The majority of people present at the meeting
favored the most radical solution (**). Given such a change,
the semantics of architectural specifications would then be
rewritten accordingly (becoming institution independent on the
way), and some sharing analysis would be described with the
status of an annex that can be used to discharge the extra
verification condition in the typical cases.
This change requires some minor adjustments in the summary.
==============================================================================