[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Tentative Language Design Summary version 0.93 available
Dear friends,
after settling the remaining questions for subsorting (there are only very
few things to decide at the next meeting) due to a very productive meeting
here at Bremen and subsequent work on the details (including Maura!!) we
effectively have the formal semantics for them as well. So far so good.
What bothers me are some open questions for me related to structured and
architectural specs. I think Peter apparently did a very good job at
putting into the document what was the result of the last meeting +
Dagstuhl, but then the discussion became somewhat stuck, partially due to
the fact that Michel is very busy with more important matters (so he
convinced me). So we urgently need a meeting on this; since everything else
is impractical the most tangible solution is to devote about a days work at
Edinburgh; there seems to be no other way to get everybody together this
year. Whatever we can resolve by email before, the better.
Personally, I do not think we are behind schedule so much as we effectively
seem to have solved a lot of the formal semantics questions already. I
suggest we also have a meeting, however brief, about what extensions we
want; there are some besides concurrency, for example higher order,
polymorphic types, parametrized types. Note that we need to analyze these
carefully as there may be conflicts with the present solution; this
feedback is what the next phase of CoFI is about.
I suggest we do not yet discuss concrete syntax at the next meeting.
Perhaps version 1.0 should wait until after the november meeting.
Here are my remaining problems (sorry if I repeat myself):
(1) compound identifiers are too close to parametrized types and
polymorphic functions to be introduced as such; Don has also uncovered some
severe problems based on his experience and apparently problems the Larch
people had. We should drop them and perhaps think again about convenient
renaming upon instantiation or the sharing issue in general.
(2) I am still not sure I understand architectural specs. What seems to be
missing though are names for the formal parameters of UNIT-FUN-SPECs such
that they can be referred to in subsequent parameters. At the same time,
the SPEC of a formal parameter must be able to refer to a previous
parameter; this is what Pi-specs are about. Consider the standard example:
UFS: (X: ELEM) -> (LX: LIST X) -> S X LX
Furthermore LIST should be a parametrized specification (of the kind
introduced in chapter 6.3) to get a link between part II and III. I realize
that X is and algebra and not a spec; but can we not define sufficient
conditions on specs like LIST such that a "coercion" is possible? e.g. that
LIST must be persistent w.r.t. its parameters?
I (and several others) care a lot about the analogy between parametrized
specs and parametrized architectural constructs; we should not loose this
intuition. Thus, again, I vote for positional associations in 6.3 (as
apparently in 8?).
Best regards Bernd
___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner courier mail only:
FB3 Mathematik und Informatik MZH 8071, FB3
Universitaet Bremen Universitaet 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
NEW: http://www.informatik.uni-bremen.de/~bkb