Minutes of the Methodology Task Group Meeting in Cachan

[Michel.Bidoit@lsv.ens-cachan.fr]

		CoFi Task Group on Methodology
		Minutes of the Cachan Meeting

    Saturday November 7 (afternoon) and Sunday November 8 (morning), 1998.

Contents:
---------
I - List of participants
II - Summary of discussions
III - Work to be done

*******************************************************************************
* I - List of participants
*******************************************************************************

Egidio Astesiano - Michele Barana - Hubert Baumeister - Michel Bidoit -
Mark van den Brand - Maura Cerioli - Christine Choppy - Anne Haxthausen -
Heinrich Hussmann - Kolyang - Bernd Krieg-Bruckner - Till Mossakowski -
Gianna Reggio - Horst Reichel - Markus Roggenbach - Don Sannella - Pippo
Scollo - Andrzej Tarlecki - Françoise Tort - Frederic Voisin - Alexandre
Zamulin.

*******************************************************************************
* II - Summary of discussions
*******************************************************************************

II.a - User's manual
II.b - Libraries of Examples
II.c - Case Studies Repository

II.a - CASL User's Manual:
==========================

A thorough discussion related to the production of a CASL User's Manual has
taken place during the meeting (and indeed was the main topics discussed).
It is not possible to reflect here the lively discussion, and below is just
a brief summary of some points made during the meeting.

* The production of a CASL User's Manual is very important for the future
  success of CASL and should have top priority.

* According to the fact that other material is/will be available [Language
  Summary, Semantics, Rationale (to be updated), Tutorial (mainly on the
  language design, to be updated too)], where detailed, precise and
  technical information can be found, it seems preferable to adopt a rather
  "informal style" for the User's Manual (UM) and to favour a pedagogical
  presentation suitable for a large audience (possibly aware of formal
  techniques and of algebraic specifications). It can of course be assumed
  that the reader will have a basic background in math, e.g. naive
  first-order logic, partial functions. Emphasis should be put on
  understandability rather than on formal rigor.

* w.r.t. the style of the UM, there will be a clear separation (e.g. 
  typographic distinction) between the plain UM and some sections more
  directed towards the advanced user, where hints on some potential misuses
  of some features will be explained. But these "advanced user pieces" of
  the UM can be skipped at first reading.

* The presentation of CASL should be, as much as possible, "problem
  driven". E.g. first explain some problem to be specified, then show how
  to solve it using CASL. This will motivate the various features of the
  language to be explained in a problem/solution perspective. Cf. e.g. 
  Hoare's book on CSP, Booch's book on Object-oriented design in Ada.

* The UM should have plenty of examples, preferably illustrating various
  specification styles. In addition, an Appendix will detail a library of
  "approved predefined standard specifications" that will help a user to
  start to specify a given problem without having to redo the usual
  standard boring stuff. There will be room for various specification
  styles in this Appendix too.

* w.r.t. the structure, the UM will of course be internally organized
  according to a plan that will not considerably differ from the one of the
  Language Summary (see suggested plan below). However, the presentation
  should follow the "problem-driven" approach. This means that even if the
  presentation is organized in a "feature-oriented" fashion, the reader
  should rather have the feeling that along the UM, more and more tools to
  solve more and more advanced problems are given.

* Suggested preliminary structure:
  Introduction
  Presentation of some (global motivating) case studies (problems to be solved
  using CASL)
  [This presentation could either be done in a preliminary chapter or
  instead we may have an incremental distributed introduction of the cases
  in the chapters.]
  PART A
    I. Basic total specifications (with total functions and predicates)
       1. Simple axioms (e.g. conditional horn clauses)
       2. Full first-order
    II. Data Type Definition (total case only, no subsort).
       1. Simple  2. Generated  3. Free
    III. Partial functions
    IV. Subsorting
    (with some discussion on partial vs subsorting)
    (in III and IV, datatype definitions are revised and extended)
  PART B
    V. Structured specifications
    VI. Parameterized specifications and views
  PART C
    VII. Architectural specifications
  PART D
    VIII. Library - Version Control
  APPENDIX with library of standard specifications, etc.

During the meeting some people have volunteered for writing some parts of
the UM.

IMPORTANT NOTE:
===============
  During the coordinators' meeting, the issue of the CASL User's
Manual was rediscussed. The coordinators pointed out the crucial
importance of the UM w.r.t. the future visibility and success of CASL,
and they felt strongly that discussions on the User's Manual should
have been more carefully prepared in advance through e-mail
exchanges. They asked the methodology coordinator to prepare a revised
proposal for a User's Manual that will be published as a book.  As a
first step, there will be a preparation phase during which the
coordinators will discuss and agree on a detailed concrete proposal
for the User's Manual. In a second step, the selected authors
according to this new proposal will start to write their respective
chapters. The UM will be supervised and edited by the methodology
coordinator.

*** As a consequence, people who have volunteered during the meeting for
    contributing to the User's Manual are kindly asked to WAIT until some
    FIRM PLANS are agreed upon before starting any concrete work on the UM.


II.b - Libraries of Examples:
=============================

It should be clear that libraries of examples are welcome. Everybody is
encouraged to write (convincing) examples of CASL specifications and make
them available (e.g. via URLs).

On the other hand, and in particular for the Appendix of the User's Manual,
it is important to have a library of "approved" specifications, in
particular for standard data types (Natural, Integers, Sets, Lists, etc.).
Bernd Krieg-Brückner is volunteer for proposing concrete plans related to
this issue.


II.c - Case Studies Repository:
===============================

Similarly, (large) case studies using CASL are welcome. Everybody is
encouraged to provide case studies, which can either illustrate some/all
features of CASL or as well emphasize the role of CASL for
e.g. requirements engineering, formal software development, or both.
Student projects may be a good source of such case studies.
It is suggested to announce the availability of these case studies via the
methodology mailing list.

On the other hand, it is important to have a well established base of
motivating and significant case studies. A good idea may be to reuse
existing case studies in the litterature and to adapt them to use CASL as
the specification language (and moreover to fully take advantage of the
nice features provided by CASL).

In a first step, Hubert Baumeister is volunteer to establish a list of
potentially relevant case studies. For each of them it should be clarified
the amount of effort needed for their conversion to CASL, and more
importantly the class of CASL features that will be illustrated by these
case studies.

If possible, it should also be tried to develop case studies in cooperation
with industry (as announced in the Working Group proposal).

During the meeting, the following case studies have been mentionned (but
their suitability has still to be established):

Craigen/Gerhart NASA report 
OBJ3 book draft
Verona student's project
Steam Boiler
Destijl Project
Invoicing case study
ACT airport schedule, line editor
DFKI security example
PVS examples
CoQ 3D modelling example
Offside rule in football
Van Diepen Swiss system for tournement scheduling

Among the above potentially interesting case studies, it is agreed that the
steam boiler may be a good candidate for a (but not the only one) 
motivating example to be used in the UM.


*******************************************************************************
* III - Work to be done
*******************************************************************************

1. Methodology coordinator will prepare in agreement with the other CoFI
   coordinators a precise, detailed proposal for a User's Manual book,
   together with concrete plans and schedule for publication.

2. Bernd Krieg-Brückner will prepare a proposal for establishing an
   approved library of standard specifications.

3. Hubert Baumeister will collect informations related to existing case
   studies, and their suitability for being reused for CASL case studies.

4. Everybody is encouraged to write CASL examples, CASL case studies, and to
   report on their experience in using CASL as a specification language.
   In particular, notes on specific uses/misuses of CASL features are
   welcome, including revision of existing methodology notes.

Michel Bidoit
CoFI Task Group on Methodology Coordinator

PS: Many thanks to Christine Choppy for her help in the preparation of
these minutes.