[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Minutes of the Language Design Meeting at Cachan
Dear friends,
sorry to be late; I have been afflicted by some hearing problem and have
to undergo some treatment. On top of this, a bad cold put me to bed last week.
This also means that I will not be available from now to 10 Jan.
Best regards
Bernd
------------------
Minutes of the CoFI Language Design Meeting at Cachan
[Kolyang, revised by BKB]
Plenary Session
8 November 1998
Present: Bernd Krieg-Brueckner(chair), Andrzej Tarlecki, Don Sannella, Pippo
Scollo, Michel Bidoit, Maura Cerioli, Anne Haxthausen,
Alexander Zamulin, Hubert Baumeister, Till Mossakowski, Kolyang, Helene
Kirchner, Christine Choppy, Gianna Reggio, Maura Cerioli, Egidio Astesiano,
Markus Roggenbach, Mark van den Brand, Heinrich Hussmann, Horst Reichel,
Frederic Voisin, Michele Barana
Presentation by Till: Changes from CASL v.099 to CASL 1.0
----------------------------------------------------------
import and generic views
abbreviations for the writing of views
subsorts embedding do not extend to compound ids
Free datatypes have been restricted to always give free semantics
Examples have been revised
Architectural Specs
New "closed" construct for unit spec
sharing is related to the overload relation
Finalization
Semantics of CASL V1.0 almost finished (institution independent)
Parsers have to be completed and evaluated
Formatting package
Annotations (parsing, semantics ...)
Small remaining discrepancies
-----------------------------
Bernd introduces the ambiguities related to the following expression
f:t could be parsed as (op f:t) or (pred f:t). This is distinguished
in the term language but not in mapping morphism like f:t->g. Here
the decision is made context-sensitive.
Tentative solution. Add a sentence to the reference manual (section
6.2.1), where this case must be restricted.
Proposal: Bernd, Frederic and Till volunteered for having a closer
look at the problem and come up with a solution or at least a proposal.
[The resulting proposal is essentially the above: a sentence demanding that
all qualifications in morphisms etc. are "covered" by a prefix (to their left)
such as "ops/op" or "preds/pred". BKB]
How to cope with bugs in the Summary?
-------------------------------------
- there are to be no language design changes to CASL 1.0 within the
next 2 years (i.e. until the end of the WG)
- add a list of bugs or fixes (i.e. small wording changes; the above
issue is a borderline case, but to be accepted)
in a special place (not in the document)
- releases of the document are to be distinguished by date of issue
but do not lead to a new version of the language (i.e. still 1.0)
Finalization and Annotations
-----------------------------
The publication of the document is a due to the coordinator and
the annotations are Tools Issues. Peter should review the section on
Finalization to extract (and delete) items related to other issues than
language design. The aim is to cancel this section in the next release;
pointers to ongoing work should appear elsewhere in the WWW pages.
Procedure to Approve Extensions
-------------------------------
Discussion on the establishment of a procedure of how to make a
proposal for an extension to a sublanguage of CASL:
- it must be a conservative extension of a significant subset of CASL,
- while work on and around CASL should be encouraged, proliferation of
extensions is to be discouraged,
- extensions should be related as much as possible
- a document that lists the changes to CASL must be produced
- the proposal must be convincing about the semantics
...
Thus the agreed procedure is as follows
(Capitals denote milestones, "<>" denote interim work to do):
A. Initial note to the Language Design Coordinator (e.g. by email)
that an extension is being worked on
[This way, (the proposers and) other interested parties can be
informed about (other) ongoing work. Extensions should be related
as much as possible; proliferation is to be discouraged]
<The proposers produce a Proposal, listing updates to CASL,
arguing that the Proposal is an extension of a significant subset
of CASL and that this extension is conservative.
The Proposal must be convincing about the semantics, but the
details need not necessarily have to be worked out yet; thus it has
the character of a Study Note with sketchy semantics.
It should outline the intended application area.>
B. Preliminary approval of a Proposal as a potential extension
<The proposers complete the Proposal in detail>
C. Submission of Proposal as an extension of the CASL Summary plus
a document describing the semantics on a solid theoretical basis
(preferably, but not necessarily, a complete formal semantics)
<The interested public is given the chance for feedback in a
one month feedback period>
D. Approval of the Proposal
During the WG period, decisions are made by the CoFI Coordinators, thereafter
by a resp. body to be set up by IFIP WG 1.3.
[assuming that the IFIP WG approves this procedure]
HO-Extension (Presentation by Till)
-----------------------------------
Study Note L-10 has received preliminary approval as an extension
(stage B above)
===============
After Coffee Break Plenary session
Relation of CASL to programming languages: two-tiered approach
--------------------------------------------------------------
There are (at least) two ways to relate to target programming languages:
(a) consider a sublanguage of CASL (e.g. an executable sublanguage,
cf. Study Note L-9) and translate to target PL
(b) consider an extension to CASL where PL fragments are attached to
architectural specifications (i.e. units)
Proposal by Gianna Reggio for the case of JAVA
/\
| CASL [|t(SP)|]
| \//
|
| LTL Conditional
| /\
| |
p | | transformation
| |
|
| JTN (Java Targeted Notation) -- given a spec, SP
| |
| |
| | automatic translation
| \/
JAVA [|s(SP)|]
It must exist a projecton p from the domain of Java semantics to
the domain of CASL semantics such that
p( [|s(SP)|]) is an element of [|t(SP)|]
This should be possible abtract away from Java and replace it by
any other language where the relation above holds.
Summary: A study note should be produced to clarify the relation of
CASL to programming languages.
================
9 November 1998
Present: Bernd Krieg-Brueckner(chair), Andrzej Tarlecki, Don Sannella, Pippo
Scollo, Michel Bidoit, Maura Cerioli, Alexander Zamulin, Till Mossakowski,
Kolyang, Helene Kirchner, Maura Cerioli, Mark van den Brand, Frederic Voisin
Sublanguages (Presentation by Till of Study Note L-7)
-----------------------------------------------------
Proposal is to make a "hypercube" of the sublanguages, i.e. complete
the graph as much as possible; differetn views for navigation can then be
provided [a tool will be provided by Bremen].
This builds a taxonomy for sublanguages (46 have been identified
so far). The graph depicted there will have two purposes:
- for semanticists (not only CASL-semanticists) w.r.t. designing
extensions and relating external languages
- for tool developers mapping to/from other languages and from one
sublanguage to another.
It is noted with approval that the sublanguages are characterized
syntactically as much as possible.
Procedure to Approve Sublanguages
---------------------------------
The procedure should be analogous to that for extensions, but "lighter".
If possible, a schema for the definition of sublanguages should be approved,
listing attributes/properties.
With this in mind, the schema of Study Note L-7 (see above) receives
preliminary approval (stage C) as a taxonomy; comments are encouraged until 9
Jan 1999.
Small problems within the language design
-----------------------------------------
Fitting morphisms should be related to the global environment.
Example spec SP =
NAT then
List [STRING
fit ELEM |->Nat]
Proposal: import the environment and remove the local environment
There should be a discussion on the impact of the removal of the
local environment. Till sends a message to the list.
Standard libraries
------------------
There should be (a) standard predefined library/ies for numbers, characters,
strings (possibly more). For pragmatic usability of CASL, there also needs to
be a special syntax for literals, similar to programming languages. While this
is also a Tools issue, the questions is whether a syntactis extension for
literals should be
(1) just a specialized extension for the literals in the standard ADTs
(2) a syntactic extension for literals covering those in the standard
ADTs (e.g. numerals, character and string literals) but also
allowing user defined literals, e.g. for other character sets
(3) a general scheme allowing such syntactic extensions.
There is still an orthogonal issue needing a decision:
(a) signature morphisms as now, i.e. only maps A -> twentyFive
(where twentyFive needs to be defined as a constant)
(b) signature morphisms allowing maps A -> 25, i.e. a special case for
literals (more precisely terms denoting literals)
(c) terms in signature morphisms, e.g. maps A -> 4*5+5
Investigations should be made in two steps:
1. minimal extension of CASL V1.0 with BOOL, INT, CHAR, STRING, possibly
RAT, REAL, including the usual operators in infix notation (e.g. ==),
probably also standard precedences; i.e. (1) + (a or b)
2. possibility for ADTs with user-defined literals; i.e. (2)
________________________________________________________________
Prof. Dr. Bernd Krieg-Brückner courier mail only:
Bremer Institut für Sichere Systeme MZH 8071
FB3 Mathematik und Informatik FB3
Universität Bremen Universität Bremen
Postfach 330 440 Bibliothekstr. 1
D-28334 Bremen D-28359 Bremen
Telefon: (+49) 421-218-3660 telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE privat: (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb, ~agbkb
http://www.uni-bremen.de/~sppraum (Kognitive Robotik)