[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
A short case study in CASL
Dear all,
I was asked by Henri Habrias and Marc Frappier for writing a chapter
of a book intended to explore writing specifications of the same
(little) case study with several formalisms. Among the formalisms,
there are Z, B, Action systems, OMT, etc. My chapter is intended to present
the algebraic approach and I used CASL for that (I need only some
simple features of CASL). The principle of the book is to explain
step by step the development by questions/answers about the method
or about the case study. The length of the chapters is limited to 15 pages.
Below, you find requirements of the problem. If you have time and if
you are interested, you can look at the address and load the postscript:
ftp ftp.imag.fr/pub/SCOP/Papers/CASL/salg.ps
It is a draft for publication. Please, do not disseminate it.
I'll be very happy if you could do remarks either on the form (English
mistakes or incorrectnesses) or on the content (specification style).
You will be surprised by a point: in the second part of the case study,
I introduce a construction that is not CASL-right! It is the "let" (not
recursive) expression used as:
let x:T = E in F end
It seems that this construct can be replaced by:
var x:T . x = E => ... F ...
Is this the rationale for removing the let-expression from the language?
Nevertheless, the let-expression is useful when used in conjunction with
operations returning tuples of values, because, in that case, we
have to identify the (composed) result and to decompose it, in order to
use the various partial components in another expression.
I am waiting for your reactions on this point.
Another interesting point is that I speak about semantic verifications
(proof obligations) to ensure soundness of the specifications as much as
possible. This aspect is not cover for the moment by the CASL method
(to my knowledge), but I think that it should be developped further.
What do you think about this?
Thank you for your help.
Best Regards,
Didier
PS: If remarks are sent before end of August, I'll be able to take them
into account in a future version of the chapter. Otherwise, they can
be a subject of informal discussion at WADT'99 (for example).
------------------------------------------------------------------------
Requirements of the case study:
-------------------------------
- The subject is to invoice orders
- To invoice is to change the state of an order (to change it from the
state "pending" to "invoiced")
- On an order, we have one and one only reference to an ordered product of
a certain quantity. The quantity can be different to other orders.
- The same reference can be ordered on several different orders
- The state of the order will be changed into "invoiced" if the ordered
quantity is either less or equal to the quantity which is in stock
according to the reference of the ordered product
You have to consider the two following cases:
Case 1
All the ordered references are references in stock. The stock or the set of
the orders may vary,
- due to the entry of new orders or cancelled orders
- due to having a new entry of quantities of products in stock at
the warehouse.
But, we do not have to take these entries into account. This means that
you will not receive two entry flows (orders, entries in stock). The stock
and the set of orders are always given to you in a up-to-date state .
Case 2
You do have to take into account the entries of :
- new orders
- cancellations of orders
- entries of quantities in the stock
_____________________________
Perhaps you will consider that this text is incomplete. The goal of this
exercise is to know what questions are raised by your favourite method(s).
You will propose different "solutions" (expressing consistant requirements)
and you will explain how your method(s) have brought you to propose these
"solutions".
Rules for writing your text :
- Your text must be selfsufficient (you have to define, by using examples
taken in the case study, every concept and notation used in your paper. If
necessary give references to the bibliography).
- Introduce the reader to your "method":
- by relating it to other approaches (those which are nearest to
your approach, those which are furthest from your approach)
- by giving the theoretical basis (with reference to the
bibliography) - Present the questions that you had to deal with from your
method - Present the answer that you have chosen
- Show what verifications your method has permitted you to do
(detection of inconsistencies in the answers that you have chosen (ie, in
your answers express your interpretation of the case study)
Careful!
Do not extend the domain. For example, do not specify stock management
(when, following what minimum quantity to restock, etc.), do not add new
information as " category of customer", "category of product", "payment
modality", "bank account" etc.
H. Habrias, IRIN, Nantes
--------------------
Book on Comparing Systems Specification Techniques.
The objective of the book is to present different specification
techniques using a common example, the invoicing system. The concepts
of a technique will be progressively introduced as they are needed
during the construction of the specification. The book will emphasize
the specification process by highlighting the questions suggested by the
specification method and their potential answers.
We are currently preparing an example of a chapter for the book.
It has been written by Marc Frappier, who is presently visiting Nantes
for two months. When completed, we'll send you a copy for evaluation.
This example will
illustrate a pattern that each author should follow when presenting a
specification technique. There will be precise instructions on how to
structure the presentation, such that it will be easier for the reader
to naviguate through the different specification techniques covered in
the book.
We intend to select a subset of the best papers presented at the
workshop and try to cover the mainstream specification techniques. We
will also seek papers from other authors to cover other techniques. We
will ask the selected authors to restructure their paper, taking into
account the instructions and the discussions held during the workshop.
An editorial committee will make sure that the directives are consistely
followed and that the content is of high quality. Hence, the book will
certainly not be a simple publication of the workshop proceedings.
The book will also include an introduction chapter that will guide the
reader through the different techniques. An index will provide links
between the different concepts of the techniques. Another chapter will
compare the different techniques.
--------
We would like to take this opportunity to stress the importance
of strictly following the format proposed in the example chapter of
Frappier et al. Uniformity will be a key success factor for this book.
We can only submit to Springer a consistent set of chapters; publication
depends on it.
Furthermore, please note that:
- the book is not a re-publication of the conference proceedings, but a
coherent set of chapters introducing the reader to several specification
methods and facilitating their comparison;
- the notation and method must be gradually introduced in the
presentation of the example;
- the number of pages should not exceed 15;
- your chapter should be formatted according to the LLNCS style (see
http://www.springer.de/comp/authors/index.html)
--
----------------------------------------------------------------------------
Dr. Didier Bert http://www-lsr.imag.fr/users/Didier.Bert/
CNRS, Laboratoire LSR-IMAG Tel: 04 76 82 72 16 +33 476 82 72 16
681, rue de la Passerelle Fax: 04 76 82 72 87 +33 476 82 72 87
BP 72
38402 Saint-Martin-d'Heres CEDEX, France
----------------------------------------------------------------------------
----- End of forwarded message from owner-cofi-methodology@brics.dk -----
--
Michel Bidoit - Directeur du LSV
Laboratoire Specification et Verification Tel: +33 (0)1 47 40 28 68
CNRS UMR 8643 Secr: +33 (0)1 47 40 24 04
Ecole Normale Superieure de Cachan Fax: +33 (0)1 47 40 24 64
61, Avenue du President Wilson
94235 CACHAN Cedex France Email: Michel.Bidoit@lsv.ens-cachan.fr