Trip Report: IFIP WG 14.3, WADT11, COMPASS

Here is condensed version of my report on a trip last month, focusing
primarily on the parts that are relevant to those interested in Larch.


European academia still harbors a large and enthusiastic community of
researchers on the algebraic specification of abstract data types.

I am more optimistic about the prospects for developing a "common
framework" for algebraic specifications under the aegis of IFIP WG 14.3
than I was prior to this trip.  (This is not entirely due to their
interest in building on ideas from, and experience with, Larch :-).
See URL http://www.daimi.aau.dk/~pdm/Common/ 

Touristic note: If you only do one thing in Norway, take the (unguided)
"Norway in a Nutshell" tour organized by the Norwegian State Railway--but
allow more than one day for it.


Last February, the organizing committee of the 11th Workshop on Abstract
Data Types (Ole-Johan Dahl, Magne Haveraaen, and Olaf Owe) invited John
Guttag and me to choose one of us to be an invited speaker at WADT11 in
Oslo, Sept 19-23.  John couldn't go, and I thought it would be nice for
Larch to be represented.  Also, Jane is half-Norwegian, we hadn't been to
Norway for 22 years, and it looked like a good opportunity to combine
business with pleasure.

I was further invited to observe a meeting of the IFIP WG 14.3 (Foundations
of Systems Specifications) just before WADT11, and a preparatory meeting to
develop a position statement for discussion by WG 14.3 on a "unifying
framework" for system specification.

When it came time to supply my title and abstract, I still hadn't given
much thought to what I was going to say, so I picked the relatively non-
committal "The Larch Shared Language: Some Open Problems."  (There are
always open problems.)  When it was time to prepare the talk, I solicited
input from other Larchers and combined it with messages that I had filed
concerning possible future developments of LSL.  In the event--somewhat to
my surprise--the slides I prepared helped me to say just what I wanted to
say after hearing the WG 14.3 deliberations and the first half of the

The meetings were all held at Soria Moria, an excellent residential
conference center owned by the Norwegian Medical Association.  Oslo is "one
of the world's largest cities (175 square miles)."  Soria Moria is in the
city limits, but in a very rural area at an altitude of 500 meters with a
great view over fjord, forest, some residences, and a little industry.  It
is up the road past the famous Holmenkollen ski jump; our taxi driver said
it was the most exclusive neighborhood in Oslo, with homes in the $500K to
$1M range.

    Soria Moria (So'-ria Mo'-ria) is a name invented by Edvard Grieg for
    a wonderland that can never quite be reached, but only glimpsed on the

      IFIP WORKING GROUP 14.3 (Foundations of Systems Specifications)

This was my first 14.3 meeting, and some of the position papers that had
been circulated were (in my opinion) excessively grandiose in their goals,
so I came prepared to observe with my mouth shut.  This was impossible,
because my opinion was repeatedly solicited.  (At one point, the three
"practical" specification languages were declared to be OBJ3, Larch, and

In the pre-meeting, I pushed for minimalist goals ("The most important
decisions in language design are what to leave out."--N. Wirth), and
suggested that everyone in the room would have to sacrifice at least one
feature he/she considered very important (and even got one volunteer to do
so).  I also pushed for a design process that made a single person
responsible for the conceptual integrity of the entire framework, rather
than design-by-committee.  After my speech on the subject, Bernd Krieg-
Brueckner volunteered to take this responsibility and chair the language
design committee (and was accepted by acclamation).  So I may have done
some good.

A clever way to make progress without requiring permanent sacrifice was
devised: The committee will focus on a "level 1" core language whose design
can be completed in a year, because it contains only those things that are
straightforward and uncontroversial.  All the researchy stuff--like
concurrency and sort inference, and probably higher-order logics, and maybe
sophisticated forms of subsorting--will be deferred to "level 2."

The main meeting went over some of the same ground, with the aims
identified by the pre-meeting listed as Applicability, Accessibility,
Urgency (tangible results for the ADT community in less than a year, for
industrial use in three years), Unifying property, Science, and Support of
multiple methods.  Work products would be a Reference Manual, a User
Manual, a textbook, and supporting tools.

I was also asked to prepare and give a brief presentation on lessons from
Larch.  I decided to focus on just one aspect: the separation of concerns
enabled by the two-tiered approach.  My key slide was:

  Not in LSL:                       Not in interface languages:
  -----------                       ---------------------------
  State                             Theory definition
    storage allocation              Theory operations
    aliasing, side-effects            inclusion, assumption, implication,
  Control                             parameterization
    errors, exception handling,     Operator definitions
    partiality, pre-conditions      Facilities for libraries, reuse
  Programming language constructs
    type system, parameter modes,   i.e., all the subtle, hard stuff
    eccentric notations & syntax
    *all* operators are auxiliary
  Design of a programming language

  i.e., all the messy, boring stuff

          Mostly, features in the two tiers don't interact.

In the following coffee break, people I'd discussed Larch with many
times came to me and said things like "This is the first time that I've
understood the point of having two tiers."  So I guess, even after all this
time, it's still worth focusing on a single point, rather than covering a
whole range of issues.

Five heavily overlapping subcommittees were formed (by self-selection):
Language design, Methodology, Formal semantics, Tools, Reactive systems.
The language committee is to report initial progress at a meeting in Paris
on November 17.

I was impressed by the seriousness of this effort.  I believe that the
meeting consensus was for two much more attainable goals than those implied
by some of the pre-meeting position papers: 

+ Design common syntax and terminology for what the main algebraic
specification languages have in common, to remove needless differences
resulting from history and arbitrary choices.

+ Reduce the number of languages under development, rather than adding yet
one more.

This effort bears watching.  I indicated that the Larch community would be
interested in harmonizing compatible features with the common framework, as
it emerges.

Bernd decided to hold the first meeting of the new language design
committee immediately following the WADT meeting, "to take advantage of
Jim Horning's presence."  About 20 people, in addition to the 8 members
of the committee, crowded into the room, and for about 90 minutes treated
me somewhat as an oracle--a novel and not entirely comfortable experience.
My answers may have been cryptic, but I hope I succeeded in following the
Hippocratic injunction, "First, do no harm."


For practical purposes, these were the same.  COMPASS is an ESPRIT basic
research initiative of the European Community that funds travel for
cooperative work on formal specification techniques, in particular,
attendance at WADT.

WADT11 was an interesting hybrid of a workshop and a conference.  It
consisted mostly of paper presentations followed by discussions, but there
were about a hundred attendees and about sixty papers--many with multiple
authors in attendance--plus six invited talks (by Hartmut Ehrig, Rod
Burstall, Tony Hoare, Pierre Lescanne, Egidio Astesiano & Bernd Krieg-
Brueckner, and me).  So most everybody got to talk.

    The attendees were mainly European professors and their graduate
    students, plus two American "industrialists"--Eric Wagner of
    Yorktown Heights and me.  Algeria 2, Belgium 1, Denmark 1, Finland 1,
    France 11, Germany 31, Italy 3, Lithuania 2, Netherlands 6, Poland 4,
    Portugal 4, Romania 1, Spain 1, United Kingdom 9, USA 3, Norway 14.

Here are brief notes on talks that may interest Larchers:

++ Peter D. Mosses <pdmosses@brics.aau.dk>, "Combining Algebraic and
Set-Theoretic Specifications."  "We propose an intermediate framework where
algebraic specifications are enriched with a set-theoretic type structure,
but formulae remain in the logic of equational Horn clauses.  This combines
an expressive yet modest specification notation with simple semantics and
tractable proof theory."

++ Olaf Owe <olaf.owe@ifi.uio.no>, "On the Use of Subtypes in ABEL:
Syntactic Control."  Terminating Generator Induction.  Optimal profile set
generation from function definition (terminating fixpoint computation).
Strict generators.  Syntactic subtypes help make rewrite rules strict.
Semantic subtypes help to obtain one-one basis.

++ Pierre Lescanne <Pierre.Lescanne@loria.fr>, "On the Relations between
Rewrite Systems, ADTs, and Lambda Calculus."

++ Christine Choppy <cc@lri.lri.fr>, "Interchange Format for
Inter-operability of Tools and Translation: The SALSA and Asspegique+/LP
Experience."  "We present our experience in using tools developed for other
specification languages than ours, and that were connected with our usual
environment.  When working with different tools, we identified various
sources of problems, and we developed a generic way to make this connection
possible that uses a particular interchange format."

++ Eric Wagner <EricWagner@aol.com>, "Guarded Algebras and Data Type
Specification."  Another attack on the problem of "how to write
specifications when there are things that you don't want to specify."  Eric
rejects the semantic complexity of Error Algebras and Partial Algebras, and
the syntactic complexity of explicitly writing all the axioms that seem to
be needed to define all the cases that arise in typical domains with errors
(such as division by zero or taking the top of an empty stack).  His
solution uses total operations and conditional (guarded) axioms, and then
exploits the properties of guards to avoid writing lots of boilerplate.  We
solved this problem another way in Larch, but this is the second-best
solution I've seen. :-) Technical report (with Magne Haveraaen) in

  My own talk, "The Larch Shared Language: Some Open Problems."  It turned
out that several of the topics I selected for this talk were among the
most-debated in the WG 14.3 discussions on a "common framework," so I was
given almost the last word on: sort systems and subsorting, total vs.
partial functions, composition mechanisms, and underlying logical systems.
(My slides are at URL http://www.research.digital.com/SRC/larch/WADT11.ps )

			       TRAVEL NOTES

[I cannot resist including this excerpt.]

Weather: Reputed to be rotten (wet and cloudy) this time of year, but you
couldn't prove it by us.  We encountered some rain, but most times when it
counted we had lovely sunny but brisk weather.

Norway in a Nutshell: The Bergensbanen from Oslo to Bergen was considered
one of the railway engineering triumphs of the early 20th century.  292
miles, 200 tunnels, nearly 100 miles above tree line.  The Norwegian State
Railway has organized a short (60 mile) detour via local bus, ferry, and
"one of the world's most spectacular branch railway lines" that, in a small
space encompasses most of the types of scenery for which Norway is famous
(except glaciers).  For this unguided tour you get a ticket and a schedule
of connections; how long you spend is up to you.  We should have allocated
more than a part of a day (on the way from Bergen to Oslo) to it.

The 85-minute bus trip from Voss to Gundvangen was splendid.  The high
point was a 10-minute stop at Hotel Stallheim--the only hotel I've seen
whose location is definitely superior to the Ahwani in Yosemite and the
Grand Canyon Lodge.  We should have planned for at least a day there.  Then
the highway plunged to the tip of one of the branches of Sognefjorden, the
longest and deepest of Norway's fjords.  We took the ferry from there to
Fl{\aa}m, at the tip of the next branch east--a two-hour ride.  Think of
four Yosemites (minus Half-Dome) with 340 meters of water in the bottom,
and {\em lots} more waterfalls.

Due to a scheduling glitch, we did not get to take the branch line train
from Fl{\aa}m to Myrdal, but instead took a bus provided by the railroad to
rejoin the main line at {\AA}l.  Mostly in the dark, but quite scenic until
the moon went down.  Unfortunately, the interior lights on the train were
so bright that we saw no scenery from {\AA}l to Oslo.