[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Minutes of the Cachan meeting
TOOLS GROUP MEETING
Cachan, November 10-11, 1998
Participants:
=============
Egidio Astesiano,
Hubert Baumeister,
Michel Bidoit(*),
Maura Cerioli,
Christine Choppy,
Heinrich Hussmann,
Helene Kirchner(*),
Kolyang(*),
Bernd Krieg-Brueckner(*),
Till Mossakowski(*),
Gianna Reggio,
Horst Reichel,
Wolgang Reif,
Markus Rogenbach,
Jerome Ryckbosch (EDF),
Don Sannella,
Pippo Scollo(*),
Andrzej Tarlecki,
Francoise Tort,
Mark Van den Brand(*),
Frederic Voisin(*),
Alexandre Zamulin.
Participants marked by (*) partipated to the restricted
group meeting on Tuesday 10 in the morning.
AGENDA
======
Summary of objectives
Summary of the work done
- status report of the various parsers
- CASL package for LaTeX formatting
- interchange format
- HOL-CASL
Future plans
- Parsing
- Editing
- Annotations
- Sublanguages of CASL
- Rewrite engine(s)
- Proof environments
- Approval procedure for tools
- Making our tools available to the community
====================================================================
I. Report on the various parsers
Different parsers have been developed to make sure that the CASL
syntax is parsable using standard technology. These parsers
were developed concurrently with the concrete syntax, which was
inconvenient for the parser developers but had the advantage to help
detecting ambiguities and inconsistencies in the syntax.
Here are below the caracteristics of these parsers (order is not relevant):
+ Christophe Tronche (Cachan): LL(2) parser generated by the C++
version of PCCTS.
Produces a tree in CSF format (A-term like).
Mixfix parsing and annotations not supported yet.
The parser is available at
http://www.lsv.ens-cachan.fr/~tronche/cofi/
+ Frederic Voisin (LRI): LALR(1) parser based on SYNTAX
a parser generator developped at INRIA.
Produces a tree in CSF format.
Mixfix parsing not supported.
>From these two, only the first one is going to be maintained.
The second will be used for checks.
People are encouraged to use the first parser and send their
CASL specifications to Frederic Voisin.
+ Kolyang and Till Mossakowski (Bremen): based on the generic parser
of Isabelle.
Produces an ML data structure corresponding to an abstract syntax tree.
Restricted to basic specifications.
Supports labels and comments.
Mixfix parsing not supported yet.
Information is provided at
http://www.informatik.uni-bremen.de/~agbkb/library/CASL/
or
http://www.informatik.uni-bremen.de/~cofi/library/CASL/
+ Bjarke Wedemeijer (Aarhus and Amsterdam):
based on SDF and GLR parsing, generated from an SDF definition of CASL.
produces a term of the abstract syntax, which can be converted to
the ATerm format.
Mixfix parsing and annotations are supported.
Bjarke Wedemeijer's Master Thesis available as a Technical
Report from U.of Amsterdam.
http://www.wins.uva.nl/pub/programming-research/reports/1998/
File: P9809.ps.gz
This work will give a stand-alone parser before the end of 1998.
+ Hubert Baumeister (MPI): parser developed with JAVACC.
More information will be provided soon.
Hubert also made a Prolog program that parses the EBNF grammar
of the concrete syntax and produces from a textual representation
of the grammar
- either a set of Prolog clauses
- or a set of EBNF rules.
http://www.mpi-sb.mpg.de/~hubert/CoFI
====================================================================
II. LaTeX and HTLM formatting
The goals are to provide help for
- uniform formatting of CASL specifications
- combining parts of document by different authors
- pretty-printing CASL specifications
- converting from LaTeX to HTML
Peter Mosses has written CASL packages for LaTeX and Hyperlatex
http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary-v1.0/casl.sty
http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary-v1.0/casl.hlx
Updated documentation for the CASL package be available very soon.
See Peter's note: formatting CASL specifications using LaTeX
http://www.brics.dk/Projects/CoFI/Notes/C-2
Peter plans to adjust the CoFIdoc package
http://www.brics.dk/Projects/CoFI/Notes/C-1-1.1/
to accomodate pdflatex too.
====================================================================
III. Interchange format
The Annotated Term Format
http://www.brics.dk/Projects/CoFI/Notes/T-7
has been selected on the following criteria:
- Experimented in ASF+SDF and in other CWI groups.
- Tree representation well-suited to represent programs, specifications,
abstract syntax trees, proofs...
- Provide annotations to store computed results relevant for other tools
- Libraries for Aterms and associated operations in C and JAVA
to parse and unparse Aterms, create and manipulate A-terms.
This library is available at url:
http://www.wins.uva.nl/pub/programming-research/software/aterm/
File: aterm-0.10.tar.gz
====================================================================
IV. HOL-CASL
HOL-CASL is an encoding of CASL into Isabelle, that can be used for
theorem proving in CASL-Specifications.
HOL-CASL consists of four parts:
-- Parsing of the input text (see above).
-- Static semantic analysis, including overload resolution,
which checks if an abstract syntax tree corresponds to a well-formed
CASL specification and constructs a theory in SubPCFOL, the underlying
institution of CASL.
-- Encoding SubPCFOL into Isabelle/HOL via a map between the underlying
institutions of the logics.
-- A graphical user interface
See
http://www.informatik.uni-bremen.de/~agbkb/library/CASL/
====================================================================%
V. Parsing: Future plans
-0- Development of a repository with successfully and
unsuccessfully parsed specifications, to be used as tests for parsers.
This task can begin now. The repository initialized by Christophe Tronche
(http://www.lsv.ens-cachan.fr/~tronche/cofi/)
will be used for that.
-1- Comparison between the available parsers:
they may differ when some ambiguities are interpreted in different ways.
This comparison will be based on the definition of
a common output format for the different parsers (A-term like).
Frederic Voisin and Mark van den Brand are going to propose an output format
and to perform comparisons between their parsers.
-2- Mixfix parsing.
To added to Christophe Tronche's parser.
-3- Determine a reference parser for CASL.
Creation of links to other parsers.
-4- Static semantics analysis. (Mixfix parsing may need a part
of static semantic analysis).
====================================================================
II. Editing: Future plans
- Development of a structure editor and of an Emacs mode.
ASF+SDF tools able to produce them will be publicly available
within six months.
- Graphical interface.
Based on DaVinci Christine Choppy will propose a tool to display
the structure graph of CASL specifications.
====================================================================
III. Annotations
Needed for parsers, rewrite engines, proof tools.
See Till Mossakowski's note for parsers and static semantic checkers
http://www.brics.dk/Projects/CoFI/Notes/T-6
In A-terms, annotations are again A-terms and can be structured.
We need to:
- Identify annotations relevant for each class of tools.
- Classify annotations into user annotations and tool annotations
that may be local or global, i.e. of interest for all tools.
- Define an abstract syntax for annotations.
- Provide means to select relevant chunks of annotations for each tool.
The set of annotations has to be controlled: a list of approved
annotations will be determined by the Tools group and available on the
Web page for Tools. A proposal for a new tool will have to include a
list of relevant annotations and new ones will be approved by the Tools group.
Based on his previous note, Till Mossakowski will propose a format for
annotations and a preliminary list of annotations.
Below is a preliminary list where items are prefixed by U (Users)
or T (Tool) according to creation of the annotation.
-U- User comments
For parsers:
-U- layout, priorities/precedences
-U- aliases
-U- labels
-T- syntax error messages, line numbers
-T- sublanguage
For static semantic checkers:
-T- local environment : inherited specifications and signatures,
profile or sort of symbols
-T- error messages
-T- expanded forms of constructs
-T- proof obligations to guarantee well-formedness
For rewrite engines:
-U/T- ordering (for equalities)
-U- AC attributes,
-U/T- sort of terms, built-ins
-U- name of rule
-T- normal forms of terms
-T- failure with rule label
-T- visibility (global/local), module
-T- sublanguage
For proof tools:
-U/T- name of proof
-U/T- classification: axiom, proof obligation, user lemma
-T- status: proved / unproved
-T- list of theorems used in a proof
-T- special use of a formula: e.g. for rewriting
-T- proof obligations
-T- sublanguage
====================================================================
IV. Sublanguages of CASL
This topic is discussed also in the Language Design group.
- Which restrictions ?
See Till Mossakowski's note:
http://www.brics.dk/Projects/CoFI/Notes/L-7
for identification of `interesting' sublanguages and mappings from
sublanguages of CASL to existing specification formalisms.
- In the Tools group, the notion of `interesting' sublanguages is
driven by the existence of tools. For the time being, we expect tools
at least for many sorted equational Horn Clauses. Many sorted Horn
Clauses with any predicates have to be considered too. Many-sorted
first-order logic is addressed by the KIV system.
====================================================================
V. Rewrite engines
Two rewrite engines are planned to be connected with CASL.
The ELAN compiler:
- many-sorted conditional equations (+ strategies)
- AC patterns
- written in JAVA, produces C code
http://www.loria.fr/equipes/protheo/PROJECTS/ELAN/elan.html
The ASF+SDF compiler:
- many-sorted conditional equations
- associative lists
- written in ASF+SDF, bootstrapped, produces C code
http://www.cwi.nl/~gipe/asf+sdf.html
====================================================================
VI. Proof environments
ISABELLE (see HOL-CASL at Bremen)
KIV : Wolgang Reif made a presentation of KIV pointing out
similarities and differences between the KIV and CASL specification
languages, then showing the potentiality of KIV as a specification
and proof environment, and its applications.
See
http://www.informatik.uni-ulm.de/pm/kiv/kiv.html
[As pointed out in a following message, the URL originally given here
was completely outdated - sorry!]
Bernd Krieg-Brueckner and Michel Bidoit volunteer to study with the
KIV group the precise sublanguage of CASL handled by KIV.
The possibility of modifying the concrete syntax of KIV to conform to
CASL concrete syntax is addressed: the obvious advantage would be to
avoid back and forth translations that may be painfull in the
interactive setting of KIV. The problem has to be studied by the KIV
group.
Several other contacts have been taken, especially with:
SPIKE, an automatic theorem prover in equational Horn logic.
http://www.loria.fr/equipes/protheo/PROJECTS/ELAN/spike.html
INKA, a first-order theorem prover with explicit induction.
http://www.dfki.de/vse/systems/inka/
====================================================================
VII. Proposal and Approval for a new tool
A 3-steps process is proposed:
-1- A proposal consists of a presentation of the tool addressing the
following questions:
- which is its purpose?
- which sublanguage of CASL is addressed?
- is the tool conform to the CASL syntax?
- is the tool conform to the interchange format?
- which are the relevant annotations?
- how to use it?
- how to install it?
To be proposed a tool must either accept (a subset of) the CASL syntax,
or accept the interchange format of A-terms and respect the approved
set of annotations.
-2- A feeback period of one month will follow the announce of the proposal
in the CoFI mailing lists.
The tool will be tested by CoFI members and comments will be recorded
during this period.
-3- After this period, a label will be given to the tool according
to the received feeback by the Tool coordinator.
Possible suggested labels are:
experimented, in experimentation, not yet experimented.
The labels will be regularly updated.
Which are the benefits for a tool proposer:
- based on available ressources, the Tools group will give
a close look at the proposed tool and constructive feeback.
- free access and connection with other CASL tools
includig the repository of examples and CASL library.
- advertisement of the tool in CASL presentations.
====================================================================
VII. Making our tools available to the community
We plan to have:
-1- A Web page for tools with
- on-going works and interests
- available tools
- how to propose a new tool
-2- An integration platform for our tools based on the Uniform
Workbench in Bremen or on the ToolBus in Amsterdam. Both sites are
expected to provide advice and expertise for integrating new tools.
====================================================================
====================================================================