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