Minutes of the Tools task group meeting

[Michel.Bidoit@ens.fr]

			........................................
			Natural languages are context-sensitive,
			German is,
			"Topferpalatshinken" is not "Shinken"
					Bernd Krieg-Brueckner
			........................................


		+------------------------------------+
		| MINUTES OF THE TASK GROUP ON TOOLS |
		+------------------------------------+


This is the minutes of the task group of the COMMON FRAMEWORK
INITIATIVE (in short CFI) on tools.

To report what was discussed and decided, I took the following
schema. First, I reported what we decided and then in a following
section, I reported important points (for me) we discussed.

			The secretary: Pierre LESCANNE
  	            -o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-

[ Thanks a lot to Pierre Lescanne for having prepared these minutes and
to Christine Choppy for having pointed out a few inaccuracies in the
preliminary version -- Michel Bidoit ]

Participants: 
------------

Hubert Baumeister, (HB)
Michel Bidoit (chairman), (MB)
Christine Choppy, (CC)
Radu Grosu (RG)
Bernd Krieg-Brueckner, (BKB)
Pierre Lescanne, (PL)
Peter Mosses, (PM)
Olaf Owe, (OO)
Gianna Reggio, (GR)
Andrzej Tarlecki (AT)
Martin Wirsing, (MW)

On a proposition of the chairman, we discussed of three chapters:
	- impact of tools on language design
	- the tools we wish to have
	- preparation of the questionnaire for the catalogue of existing tools 

A - IMPACT OF THE TOOLS ON THE LANGUAGE DESIGN
==============================================

1. It has been decided to start a new subgroup (common to the Language Design
and the Tools task groups) for designing the concrete syntax(es) of the CFI
language(s). Members: BKB, PM, GR, MB, RG, CC.

This subgroup will in particular take care of the organizational issues related
to the design of several (if needed) concrete syntaxes, provide actual concrete
syntax(es), make proposals w.r.t. how to handle comments and tool-related
annotations, and make proposals w.r.t. how to handle/restrict "ambiguity" (such
as e.g. those raised by combination of overloading, coercions, mixfix syntax,
etc.)

Notes on the following topics will be prepared:

	[1a] Motivation for various concrete syntaxes: CC, GR

	[1b] How to integrate annotations (comments,
	informations,...)? PM 

	[1c] Overloading, coercion, misfixed syntax, precedence: BKB,
	GR, MB, CC, OO

2. Lex, Yacc or more sophisticated tools? PM, RG, OO

3. Various views (presentations) of the same specification? CC, MB.

4. Annotations for Tools (why? which kinds?): PL.

5. To which extend, implicit informations should be given explicitely?
e.g. type checking vs type inference: RG.

Discussion:
----------

1a. Are various concrete views of the same specification desirable? (E.g. short
operation names vs long ones, infix notation vs functional notation, etc.)

1b. Informations should be inserted ("hooked") somewhere in the
syntax, it is usually "hooked" to a term/formula of the language.  An
annotation can be
	- a type (in the case of type inference), 
	- the kind of language or the kind of logic which the term/formula
	belongs to.   For  instance, the  language in question  can be
	equational logic, first-order logic, second order logic, a
	logic with a given level of quantifiers alternation etc.
	- an annotation specific to some tool (e.g. ordering between function
	symbols).

1c. Is this static semantics? Is it the correct place for it?
Discussion on the need for a context sensitive syntax. The discussion
continued over lunch (see the front quotation). This should be
discussed with the methodology group.

2. Influence of languages like Java and html.

5. This work should be joined with the methodology group.

In general: Theorem provers might have influence on the language. 

B - THE TOOLS WE WISH TO HAVE
=============================

We abandoned a classification proposed by Peter Padawitz in three
parts: Tools for specification design, tools for testing and executing
specifications, theorem provers. We chose a classification into two
parts.

			 --------------------
			 Minimal set of tools
			 --------------------

Syntax and static semantics checker and/or parser for the full CFI.

Latex style (compatible with lncs.sty) for CFI.

Tools for embedding existing languages and tools into CFI.

			----------------------
			Desirable set of tools
			----------------------

Syntax directed editor for the full CFI (specifically an emacs-mode)

Pretty-printer 
	latex (production of a latex source file from a specification)
	graphical representation
	index (cross-referencing)

Browsers
	component graph
	development graph
	versions

Searching facilities

Prototyping tools

Sublanguage identifiers (cf annotations)

Theorem provers
	size of the specs you can treat
	what kind of axioms?

Verification systems

Transformation systems

Methodology-driven tools

Communication tools (for cooperative work)

Translator from (to?) other specification languages.

Discussion
----------

We should 
	- clarify the minimal set of tools,
	- study how to communicate between tools,
	- study how to integrate tools
	- get feedback from the language design task group...


Internal Forms (IF) with their annotations are a way to communicate
between tools and from the parser to a specific tool.

The definition of what we mean by a "verifier" was recalled.  It is a tool to
prove the correctness of a specification (or of a refinement step): it
generates assertions to be proved by a theorem prover.


C- PREPARATION OF A QUESTIONNAIRE FOR THE CATALOGUE OF EXISTING TOOLS
=====================================================================

IMPORTANT NOTE: MB/PM will prepare the final version of the questionnaire.
What is below is NOT the questionnaire. Please do not answer it ! If you feel
that some important issues are missing, please send an e-mail to Michel Bidoit
(Michel.Bidoit@ens.fr) and to Peter Mosses (pdmosses@brics.dk).

			  -----------------
			  General Questions
			  -----------------

BASIC INFORMATION
-----------------

Availability / support
	platform/ OS/ X-W/ necessary tools 
	object or source distribution
	public domain? Licence? Costs? Nominal cost or shareware?
	cost of the necessary tools

Status: experimental? distribution version? planed?

Goodies and weaknesses

Interactive or (fully?) automatic

Applications
	library of examples
	success stories

Aim
	Which specification formalism is the tool aimed for? 
	Is it generic? How far?


DOCUMENTATION AND ACCESS
------------------------

Library management
	Is there any?
	description
	flexibility

User interface
	description
	easy to change?
	quality of error messages
	robustness

Level of expertise needed

Documentation
	user's manual
	internal documentation (references to written sources:
		article, PhD, technical report)
	one line help

User community: size? mailing list?

Integrated or simple tool

Relationships with other systems


INTEGRABILITY
-------------

Adaptability for integration with other tools

Architecture of the system

Underlying technology 
	for syntax checker and static semantics
	for syntax directed editor


			  ------------------
			  Specific questions
			  ------------------

For prototyping tools and theorem provers/proof checkers: 
	maximal size of the specification you can treat
	what kind of axioms, which logic.

===============================================================================