Minutes of the Amsterdam meeting

[Helene.Kirchner@loria.fr]

TOOLS task group Meeting

Amsterdam, September 27, 1997


Written by Helene Kirchner from the notes taken by Christine Choppy
and Christophe Ringeissen.  


Participants:

Hubert Baumeister (HB)
Jan Bergstra (JB)
Didier Bert (DB)
Michel Bidoit   (MB)
Peter Borovansky (PB)
Christine Choppy (CC)
Helene Kirchner (HK)
Bernd Krieg-Brueckner (BKB)
Karl Meinke (KM)
Peter Mosses    (PM)
Christophe Ringeissen (CR)
Mark Van den Brand (MVB)
Frederic Voisin (FV)

AGENDA:

- Parser implementation
- Interchange format
- Latex style and formatting in general
- Emacs mode
- Sublanguages
- Next meeting

See the URL
http://www.brics.dk/Projects/CoFI/Documents/CASL/Tools/
for the previous state of the group discussions.

I) Parser:

Competences for parser implementation are in Amsterdam, Bremen and Paris.

The group decides to provide a stand-alone parser able to check the
syntax of a CASL specification. It will be done in Paris under the
responsability of CC, MB and FV. This parser will be
architecture-independent, will use public domain software (on Unix
platform) to produce abstract syntax trees.  A first experimental
version of this parser will hopefully be available by the end of 1997.

This parser is not intended to be a front-end for each environment
developed by the partners. If a partner is interested in using CASL in
his(her) own environment or in an existing framework, (s)he has to
develop his(her) own parser (but this is not mandatory).  For this
purpose, a list of expected/future tools concerning parsing facilities
has to be initialised and maintained on the Web.

An encoding of CASL in Isabelle has already been done in Bremen and 
has to be updated with the agreed concrete syntax.
BKB will provide a summary and a Web-page address.
This work will be demonstrated at the next meeting.

Other problems dicussed and not resolved:
- parsing fragments of specifications, 
- need for a certification procedure for parsers developed for different
environments.


II) Interchange Format

Three existing formats have been proposed: SALSA format, A-terms
(annotated terms) of ASF+SDF, Z interchange format in SGML

For October 6, one-page abstract should be provided on each format:
- on A-terms (MVB)
- on CORBA (BKB)
- on SGML (PM) (see also Magne Haveraaen's note
http://www.brics.dk/Projects/CoFI/Notes/T-1).
A common example will be chosen and illustrated in each proposition.

Conversion between these different formats should be then studied.

Another problem to solve is the representation and extraction of
fragments.


III) Formatting

PM will provide before the end of October a LaTeX package compatible
with lncs and seminar packages for formatting CASL specifications
(with markup commands based on the abstract syntax, but producing
concrete syntax display format).
A translator LaTeX to HTML will be provided also.

Other formatting tools are needed
from the interchange format to LaTeX, HTML and RTF.

For providing an Emacs-mode for CASL: a volunteer is needed
(typical short-time project for students!).

CC will propose a tool for the display of structured specifications as
a graph.


IV) Sublanguages. Languages embedded in CASL

There are two complementary directions:

- a theoretical one: relate the institution corresponding to an 
existing language to the semantics of CASL
(cf Maura Cerioli and Till Mossakowski's works).
In general this will not be an embedding, but a common part 
should be found.

- a practical one: check if a CASL specification is a part of a
sublanguage (e.g. many-sorted equational Horn clauses), translate it
to a specification in the sublanguage (e.g. ELAN), reuse an available
tool of the sublanguage (e.g. the rewrite engine of ELAN to provide an
evaluator).

For the second direction, we should ask people who have made tools to
explain under which restrictions their tool could be used for CASL
specifications. This would allow to show which tools can be used, and to
accumulate information on needed annotations.

To relate other languages to CASL, we can provide a preliminary
version similar to PM's paper CASL for ASF+SDF users.  Other candidate
languages: LPG, Larch Specification Language, ELAN... The tools group
cannot commit himself to compare every existing algebraic
specification language with CASL.

A lot of algebraic specification languages are operational via
rewriting tools.  The priority is to have a rewriting engine for a
subset of CASL.
Connections to theorem proving tools are then strongly encouraged
and needs volunteers.

V) Next meeting in Bremen, 9-11 January 1998.