Minutes of the Paris meeting

[Helene.Kirchner@loria.fr]

TOOLS task group Meeting

Paris, January 18-19, 1997

Participants:

Didier Bert (DB)
Michel Bidoit   (MB)
Christine Choppy (CC)
Helene Kirchner (HK, chair)
Bernd Krieg-Brueckner (BKB)
Peter Mosses    (PM)
Giuseppe Scollo (GS)

AGENDA:
- Concrete Syntax
- Interchange format
- Parser
- Latex style 
- Emacs mode
- Desirable set of tools
- Next meeting

The two main achievements of the meeting were to clarify 
the different formats needed for tools on one hand, 
and to identify some requirements on the concrete syntax
on the other hand.


I. Clarification of  the different formats needed for tools.

Four formats were identified: Plain, Preferred Presentation, Interchange 
and Interoperability formats. Their use and an informal description 
are given below for each of them.


1. Plain Format 
---------------
Use: for e-mail, Emacs editing.

This is a plain text representation, readable, writable and parsable,
easily derived from the concrete syntax.

According to the different kinds of parsers applied on this textual format,
two levels are distinguished:

- Plain restricted format:
context-free parsing (for instance based on Lex and Yacc) produces
from a text in plain restricted format, an Abstract Syntax Tree ASTcf 
on which semantic analysis is applied.
This solution inherits both the simplicity and the usual restrictions 
of context-free parsing,
in particular it excludes mixfix syntax parsing.

- Plain advanced format:
Parsing is no more context-free but may be decomposed in two phases:

-- context-free parsing produces from a text in plain advanced format,
a Pseudo-Abstract Syntax Tree PAST where terms are terminals.
This intermediate structure is interesting to handle units or to give 
a view of the dependency graph of the units.

-- context sensitive parsing produces from the intermediate structure,
an Abstract Syntax Tree ASTwf where syntactical well-formedness has
been checked.

A problem to look at is the precise definition of accepted terms,
which are not the same according to these different parsers.


2. Preferred Presentation Format
--------------------------------
Use: for reading in written documents on paper or screen.

This is a graphical representation based on glyphs (digits,
letters, symbols and special characters).

It is the output format produced from the plain format by the
following tools: 
- Emacs editor 
- Pretty interactive structure editor
- CASL Font + RTF 
- Naive LaTeX : a filter transforms graphical symbols to LaTeX
macros and verbatim style is used. This is a quick and simple
possibility for producing CASL specifications in LaTeX format.
- Advanced LaTeX: this option is to provide a package of LaTeX macros
for printing CASL specifications, in the style of Paul King's package
for Z (a file CASL.sty). 


3. Interchange Format 
---------------------
Use: for exchanging parsed CASL specifications or units (i.e. incomplete 
specifications)

This is a textual representation of an Abstract Syntax Tree.
This format supports the possibility to include attributes 
and to be dynamically enriched by new attributes.
The proposed format is SGML text with some indexing method
useful to make some sharing explicit and to minimize size of files.
This is a good candidate supporting these requirements.


4. Interoperability Format
--------------------------
Use: for applying tools on CASL specifications.

All tools defined on the interchange format should 
accept the interoperability format. 
A tool may require some attributes and ignore others.
A tool must be able to work on a unit without any context.
The format needs a basic mechanism for adding attributes.
The proposed format is a slight generalisation of the interchange format:
SGML with attributes that can be classified/typed according to tools
requiring them.


====================================================================
II. Requirements on the concrete syntax
====================================================================

A concrete syntax should be provided together with examples of 
inputs and outputs and with the specification of which tools 
have been or can be applied to implement the parsing.

Any proposal should be based on publicly available and efficient 
tools, such as to Lex and Yacc

Lexical analysis should be context free and preferably in 
linear time.

The concrete syntax should support attributes and attachment 
of attributes to the right construct.

It must cover input text written with ISOLatin1 character sets
for identifiers.
A possible, additional alternative is to provide an unambiguous 
translation into the ISO 7-bit character set.

It should support nofix, prefix, infix, postfix, outfix operators.
Mixfix operators should be supported too but may be handled 
in different ways, according to parsing options.

It is desirable to allow exponents and indices in identifiers.


====================================================================
III. Plans for other (semantical) tools
====================================================================

The discussion on this topic is still very preliminary. 
These are just points that have been mentioned.

A. Different kinds of tools:

1. Prototyping tools:
A rewrite engine for the largest possible subset of CASL.

2. Generator of proof obligations related to the construction 
of modules or to the refinement process.

3. First-order theorem provers.
The proof obligations should be sent to general provers.

4. User interface and educational tools.


B. Applicability of tools

Two options are possible and maybe complementary:

1. Design or reuse of specific tools for several subsets of CASL:
equational, conditional, full first-order logic with
- total functions
- total functions with subsorts
- partial functions
- ...

2. Translate CASL to a subset of CASL (essentially total functions 
and predicates) and use available provers  
or tools for prototyping and inductive reasoning.

It should be precisely discussed how to proceed to reuse an 
existing tool.



========================================================================
IV. Next meeting: just before or during Tapsoft (Lille)
Three possibilities:
- Sunday April 13 in Paris 
- Sunday April 13 in Lille
- During Tapsoft in Lille.
Concertation is needed with other COFI tasks groups.
========================================================================