[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Minutes of Berlin meeting
Dear CASL Semanticists and Language Designers,
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...
[BKB: Andrzej's minutes also sent to the Semantics mailing list]
With best regards,
Andrzej Tarlecki
[BKB: as it turned out to be a joint meeting with the Language Design
Task Group, I am taking the liberty to add my own comments and the
minutes of the additional Language Design meeting afterwards. In fact,
I was waiting for Andrzej's minutes to do this. Many thanks to him to
be so explicit and complete!
At the end of this message I also include the minutes of the joint
meeting with the Tools group as far as it relates to Language Design,
since these minutes have not appeared yet and we need a complete view
of the potential changes.
All proposals, when put into an update of the Summary, will haved a
deadline for comments before they are formally approved. Discussion
about the proposals, if needed, should start NOW, however.
The deadline for comments BEFORE a draft of an updated summary is
being produced is next Friday (i.e. before Easter). In so far as we
had agreement in Berlin, the proposed changes will then be pretty stable.]
==============================================================================
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
Autexier, Hubert Baumeister, Michel Bidoit, Maura Cerioli, Anne
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.
[BKB: I have detailed the Language Design (LD) actions below.]
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).
[LD action: at most additional sentence in 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.
[LD action: change "symbols" to "names" in resp. sentence in 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.
[BKB: Totality has significant effects on static analysis.
Any change in interpretation of a profile such that totality
can be assumed from here onwards should be as explicit as
possible. The (only) way to do this so far is by a symbol map
effectively declaring a name to become total for a particular
profile, as in the example above. Re-declaration is illegal
and should stay that way as it is not explicit enough. The
analysis of an example in the Basic Datatypes where this was
done by mistake shows, that the example becomes more explicit
and thus better readable: a function is first declared to be
partial; later, after adding an additional axiom, it can be
proved to be total; then the re-interpretation as total in the
explicit way described above can be introduced.]
PROPOSAL: no clear-cut recommendation whether this change
should be introduced has been reached.
[BKB: My understanding of the present status of Design is that
there must be very strong reasons for a change (or they are minor
clarifications). I do not see this here unless very convincing
arguments are introduced.]
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.
[LD action: perhaps sentence of clarification in Summary.
Here, as in the other cases, methodological recommendations
should be developed eventually.]
(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 embeddings), 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.
[LD action: make adjustments to Summary, pointing out the
verification conditions and the discharge that a static analyser
is expected to make, possibly also a sufficient conditions
(e.g. in the case of specifications without subsorts.]
==============================================================================
Minutes of the Language Design Task Group Meeting
Berlin, 2 April 2000, after the above Semantics (+ LD) meeting.
Present (my apology for misspelling some names when copying from the
handwritten list; the people additonally attending w.r.t. the
Semantics meeting come at the end):
Bernd Krieg-Brueckner (chair), Andrzej Tarlecki, Agnes Arnould,
Serge Autexier, Hubert Baumeister, Michel Bidoit, Maura Cerioli,
Piotr Hoffman, Helene Kirchner, Bartek Klin, Pascale Le Gall,
Till Mossakowski, Nikos Mylonakis, Adumeur Nasreddia, Don Sannella,
Magne Haveraaen, Gianna Reggio, David Aspinall, Michael Kohlhase,
Guiseppe Scollo, Mark van den Brand.
Basic Datatypes
---------------
Markus Roggenbach presents the Study Note L-12 in the form of an
overview of the design decisions taken and the changes made since the
last version.
It is important to compare the Basic Datatypes for CASL with those for
Larch, OCL, the Lotos Standard, appendix A, Isabelle etc. Given the
amount of effort the Bremen group is already investing, we need
volunteers elsewhere!
Michel Bidoit suggests to investigate Meta Theorems about CASL to
infer some (more complex) views automatically as this might simplify
the library - an issue for the Methodology Group, possibly a tool
issue as well. Then such consequences of specifications would be made
visible by a tool (or not!), similar to implicit axioms in datatype
definitions.
The issue how to incorporate (and map down to) sublanguages is
discussed at length. The present version includes alternative styles
as well, e.g. a partial pre as well as the total version due to
subsorting. There is agreement, that the presentation of the Basic
Datatypes to users ("documentation" version that could go along with
the Summary) should make full use of CASL (and should not be
artificially restricted to a particular sublanguage) as long as this
is natural; it should be as simple as possible. On the other hand,
some "user communities" present argue for a presentation of the Basic
Datatypes in a particular sublanguage since they need this for
particular tools: no subsorts, initially specified predicates,
conditional axioms (Genova), no partial functions but loosely
specified total functions (Saarbrücken), subsorts but no partial
functions (Nancy), initially specified operations for
consistency/implementability (Bremen, see Note M-8), property-oriented
"requirement", not "operational" specification at first glance
(Cachan), ... The problem of how to structure a specification to be
able to achieve projectability ("specification for re-usability")
without having to construct several co-existing specialised libraries
is general and real. Moreover, tool support to aid this would be very
valuable. Michael Kohlhase emphasises that tool support for
presentation of a particular view may resolve some of these issues.
Perhaps the "documentation" version should indeed be a particular
derived presentation rather than the original library.
[On the way back from Berlin, the Bremen group came up with some
possible solutions that have to be investigated further].
The authors of the Basic Datatype library will make proposals for a
more "user-friendly" presentation. On this basis, it receives
preliminary approval (and applause for the work that went into it).
Comments and Annotations
------------------------
(see BKB's email of 22 march)
Note: this issue does not affect the semantics of the language, but
has to be discussed here as the Summary mentions the notations.
BKB presents the proposal originating from Till, then worked out by
BKB with input and approval from Peter. The reason for a change are
primarily feedback from work on tools.
[very brief summary of the proposal:
>
> - end-of-line comment %%... eol
> - bracketed comment %{...maybe several lines}%
>
> - commented-out text %[text, not displayed]%
>
> - general annotation %annoId ... eol
> - bracketed annotation %annoId(...maybe several lines)%
>
> - label annotation text %(labelId)% eol
The proposal is discussed in detail and summarily approved (with "very
pleased" reaction from Mark and similar nods from other tool
developers) provided the lexical issues find satisfactory solutions;
this is expected, of course - indeed, there is even hope that nesting
of different kinds of comments and annotations can be achieved (this
needs experimentation, and fast!). There is a desire that
commenting-out would also allow nesting of itself (but could not, of
course, be nested in something else; indeed, the text will be removed
before syntactic analysis alltogether). The problem of changed
notation for label annotations should be resolved by a migration tool.
Changed wording in the Summary will have to be worked out by Peter and BKB.
[As some issues about positions have been left over so far, some
proposals from BKB in this paragraph.] For structured specs, the
position issue needs a little more work, perhaps. A comment/annotation
may already appear at the beginning of a BASIC-SPEC and then annotates
this SPEC; this should take care of implies annotations after a
"then", for example. To be uniform with the rest of the proposal
(position, unless at the beginning of a list, *after* an item to
annotate it) and to avoid ambiguity, the position should be *after* a
GROUP-SPEC; in particular, this allows an annotation or comment after
any SPEC once extra braces are introduced (which then make clear what
it refers to). It is not clear to me, whether a position is needed
inside; VIEW-DEFNs. The (optional) "end" should be a position after
which a comment/annotation is generally allowed, on the preceding
LIB-ITEM. This takes care of VIEW-DEFNs and also ARCH-SPEC-DEFN and
UNIT-SPEC-DEFN as a whole. Inside an ARCH-SPEC-DEFN *after* a
GROUP-ARCH-SPEC or a UNIT-DECL-DEFN (or at the beginning of a list of
UNIT-DECL-DEFNs, in analogy to BASIC-ITEMS) should take care of
architectual specs and is in analogy to the rest of the proposal.]
Should the need for other positions of annotations arise, these will
be treated as a Tools issue; no further need is foreseen for comments.
----- end ----