[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
minutes of LD Meeting at Bonas
Minutes of the Meeting of the Language Design Task Group in
Bonas, September 16, 1999.
Remark on the Status of this Meeting
====================================
The meeting in Bonas was held for information and discussion about
ongoing work and future activity of the group. Due to the unusual time
(10.15 pm to 11.30 pm) this meeting did not make any decisions.
Attendees:
==========
Hubert Baumeister, Didier Bert, Michel Bidoit, Mark van den Brand,
Maura Cerioli, Anne Haxthausen, Helene Kirchner, Bernd
Krieg-Brueckner, Till Mossakowski, Peter Mosses, Markus Roggenbach,
Don Sanella, Lutz Schroeder, Andrzej Tarlecki, Frederic Voisin, Martin
Wirsing, Alexandre V. Zamulin, Elena Zucca.
Egon Boerger (present only for parts of the meeting)
Agenda:
=======
I. Reports on Ongoing Work
a) Response to CASL Referees
b) Parsing Annotations
c) Solution of the Brackets Problem
d) Semantic Annotations
e) Literal Syntax
f) Basic Datatypes
II. Work Items
a) Higher Order Extension
b) Extension for Late Binding / Object Oriented Extension
c) Extension by States
d) Relation of CASL to Programming Languages
e) Procedure of Approval for CASL Extensions
III. Future Meetings
I. Reports on Ongoing Work
==========================
a) Response to CASL Referees
----------------------------
Peter apologizes that the response was not ready before the
meeting. He has the intention to discuss the response with people
involved during the WADT '99. Peter will prepare a draft revised
response to the referees in october 1999, which he will make available
to both the language design and the semantics task group for approval.
Concerning the relation of CASL to other languages Michel points out
that it is enough for the response to establish only a loose relation
instead of discussing it in detail.
b) Parsing Annotations
----------------------
Bernd reports that the parsing annotations
%left assoc,
%right assoc, and
%prec
have been included in the language summary.
c) Solution of the Brackets Problem
-----------------------------------
Bernd reports that the CASL grammar allows now for e.g.
[], {}, and {||__||}
but excludes e.g.
|__| and {|__|}.
(see summary)
d) Semantic Annotations
-----------------------
Markus presents the second Bremen proposal on an annotation "implies"
with an extension from Michel.
>>>>>> Begin of the proposal >>>>>>>>>
The annotation "%implies" may immediately follow either
-> a "then" keyword within an extension; or
-> the equals sign within a SPEC-DEFN.
An annotation
Sp then %implies Sp'
is correct iff
1) Signature (Sp then %implies Sp') = Signature(Sp),
2) Sp' can be parsed as a non-empty sequence of
IMPLIES-ITEMs (see grammar below), and
3) Models(Sp then %implies Sp') = Models(Sp)
(analogously for an "%implies" immediately after the equal sign within
a SPEC-DEFN)
IMPLIES-ITEM ::= free type/types DATATYPE-DECL; ...; DATATYPE-DECL;/
| generated type/types DATATYPE-DECL; ...; DATATYPE-DECL;/
| var/vars VAR-DECL; ... VAR-DECL;/
| var/vars VAR-DECL; ... VAR-DECL
"." FORMULA "." ... "." FORMULA;/
| axiom/axioms FORMULA ; ...; FORMULA;/
<<<<<< end of the proposal <<<<<<<<<
Don proposes to include sort generation in the IMPLIES-ITEMs, i.e. to
add the line
| generated { SIG-ITEMS ... SIG-ITEMS } ;/
to the above grammar.
Andrzej points out that no annotation should change the CASL
syntax. This holds for the above proposal of an annotation %implies.
[A slightly updated proposal will be circulated shortly on this list.]
Bernd reports that the semantic annotations
%cons and
%def
have been included in the language summary. The annotation "%cons"
is proposed to be renamed into "%conservatively" to alert to its special
nature; users should be enticed to use %implies or %def instead, if
appropriate, to be able to work with easier proof obligations.
Markus presents how the annotations %implies, %def and %cons are
related:
>>>>>> Begin of the presentation >>>>>>>>>
All these annotations follow the same syntactical scheme, i.e.
SP
then %annotation
SP'
where the keyword "then" is used as structuring element that separates
the non-annotated part from the annotated part of a specification.
There is a clear distinction between the meanings of the three
annotations:
a) "%implies" vs. "%def":
For both annotations holds: any model of SP can be uniquely extended
to a model of (SP then SP').
The distinction is that in case of "%implies" the unique extension
of the model has to be the empty extension.
b) "%def" vs."%cons":
For both annotations holds: any model of SP can be extended to a
model of (SP then SP')
The distinction is that in case of "%def" the extension
of the model has to be uniquely determined.
Please note that if SP' consists only of IMPLIES-ITEMs (see the
grammar above), the meaning of the annotations "%implies", "%def" and
"%cons" is the same.
<<<<<< end of the presentation <<<<<<<<<
Till proposes to change the semantics of the already approved
annotation %cons. He points out that there exist two natural
semantics to such an notion
- a model theoretic one (which is now chosen) and
- a proof theoretic one,
which do not coincide. Till proposes to change the semantics of %cons
to the proof theoretic one.
Andrzej votes for the model theoretic semantics of %cons as everything
in the CASL semantics is done in this way. Further he points out that
the model theoretic %cons implies the proof theoretic %cons.
Michel also wants to stay with the old version.
Hubert refers to Dieter Hutter (DFKI), who argues that the proof
theoretic semantics is needed for tools and easier to handle.
[BKB: I propose that Dieter Hutter, who was not present, makes his
statement clear for a discussion on this list]
Helene sees the need for a proof theoretic %cons to deal with
corresponding proof obligations by tools.
Bernd summarizes the discussion by stating that, at the moment, there
seems to be a tendency to stay with the model theoretic %cons.
There will be
-> a proposal for %implies and a statement on %cons by Dieter,
-> a discussion period for this proposal and the meaning of %cons
of three weeks (i.e. until Oct. 24th), and
-> a final decision
There will also be a discussion on the remaining problem of the position
of annotations over the net.
e) Literal Syntax
-----------------
Bernd reports that annotations for the literal syntax of
numbers,
strings, and
lists
have been added to the language summary.
f) Basic Datatypes
------------------
Bernd reports that the note M-6 on basic datatypes in CASL has been
available since July in version 0.2. Version 0.3, which will be
correct with respect to the static semantic analysis of the Bremen
parser, is in preparation.
Open question are:
-> How "complete" are these specifications? (Do they provide the
relevant datatypes? Do they provide the relevant operations and
predicates of the datatypes?) It is necessary to compare the
specification of the Basic Datatypes with the libraries of Isabelle,
KIV, PVS, UML, ... Any help here would be much appreciated!
-> Which steps are needed to obtain a version of note M-6 for a CASL
book? The methodological guidelines included in note M-6 should
probably have a status different from the Basic Datatypes. But it is
important to discuss these rules.
Peter points out that the methodological guidelines and the basic
datatypes are intertwined. He wants not to fix things to early.
Bernd argues that there will be a book publication on CASL in near
future, where the Basic Datatypes will be included. Thus he sees the
need to discuss them.
Peter says that one should first use the Basic Datatypes before they
are published in a book. For practical purposes the datatypes should
have CASL version numbers.
Bernd agrees and proposes to rearrange the dataypes of M-6 in
libraries with version number and make them available on the net.
Markus announces that version 0.3 of M-6 inluding such a library
concept will be available in october 1999.
[BKB: there will be a split into 2 notes: one (an L-? note) including
the library of Basic Datatypes proper, and one (version 0.3 of M-6) to
include the methodological aspects]
II. Work Items
==============
a) Higher Order Extension
-------------------------
State of this project: see the talk of Anne Haxthausen at WADT'99.
Further work will address the problem of polymorphism.
b) Extension for Late Binding / Object Oriented Extension
---------------------------------------------------------
State of this project: see the talk of Elena Zucca and Maura Cerioli at WADT'99.
c) Extension by States
----------------------
There will be a proposal for a state oriented extension of CASL by
Alexandre V. (Sascha) Zamulin (Sascha) and Hubert Baumeister.
Sascha proposes to combine the extension by states and the object
oriented extension.
Bernd disagrees: there are examples of object oriented design that do
not need states. Bernd would like to deal with separate but combinable
extensions.
d) Relation of CASL to Programming Languages
--------------------------------------------
Bernd refers that up to now there is only one proposal how to relate
CASL with a programming language: the talk of Gianna in Cachan on the
combination of CASL and Java.
Bernd sees the need for a general framework for the combination of
CASL and programming languages, like the interface language of Larch.
Don says that the relation of CASL to programming languages is a
matter of the methodology task group. Only if extensions of CASL are
involved this item should be discussed within the language design
group.
Don's point of view is the final agreement at the meeting.
e) Procedure of Approval for CASL Extensions
--------------------------------------------
At a prominent point in the net there will be a Web page devoted to
CASL extensions. This page will include
-> a description of the procedure of approval
-> a list of the coordinated CASL extension together with their
status, which can be: interest indicated, tentatively approved,
approved.
For an approval it is necessary
-> to discuss the methodological need of the proposal,
-> to give a clear language description, and
-> to give a semantics to the extended language indicating that this
semantics is an extension of the CASL semantics.
For a preliminary approval, a convincing argument (but not necessarily a
fully formal elaboration) on these issues is needed; after such a
preliminary approval, such work can go on in detail.
Announcing an indication of interest implicitly means, that there is an
offer for contributing to the ongoing discussions, in a small group. The
same holds, of course, after Preliminary Approval, but discussion is
extended to the whole LD Task Group.
There are also discussions about extensions in the Reactive Task Group.
These will be discussed jointly in the two task groups once
preliminarily approved in the Reactive Task Group. There is an obvious
overlap w.r.t. the issues of state and object-orientation.
So far the status is as follows:
Indication of interest in extensions/ongoing work:
- Late Binding / Object Oriented Extension:
Elena Zucca and Maura Cerioli (Genova), Markus Roggenbach, BKB (Bremen)
- State Extension:
Alexandre V. (Sascha) Zamulin (Sascha) and Hubert Baumeister
[several people (Horst Reichel, Rolf Hennicker, Michel Bidoit, etc.) are
interested in notions of observability and/or co-algebraic extensions.
No "official" interest has been registered yet; discussions will
continue informally]
Preliminary Approval:
- Sublanguages (see LD Note L-7):
Till Mossakowski (Bremen)
- Higher Order Extension (see LD Note and draft paper):
Anne Haxthausen (Lyngby), Till Mossakowski and BKB (Bremen)
III. Future Meetings
====================
Up to small issues, which can be discussed via Email, the language
design of CASL is finished.
At this moment, there is a general feeling of the Language Design Task
Group, that its work on extensions should be, if at all, low key in
special subgroups, since work on other issues such as Methodology and
Tools, is much more important for CoFI. (Preliminary) Proposals will be
discussed once they are officially submitted.
In the future the language design task group will work in a more event
driven way, i.e. mainly coordinate and approve proposals on language
extensions.
The next meeting of the language design group will take place at ETAPS
2000 in Berlin.
----
Markus Roggenbach and Bernd Krieg-Brückner