🚀 go-pugleaf

Hello netters.

I'm posting this article for the second time and I'm sorry for
those who have already answered me (thanks very much for helping
me). I've posted this message in July, and I did receive some
answers about a part of it ; there is still an important point
I would like to solve, and that's the reason why I post this
message again :

I've just started a PhD Thesis in Computer Science, in cooperation
with a French company. The subject of the Thesis is dealing with
specification and I have to use abstraction techniques to specify
a huge software. The fact is that, today, the company didn't write
informal specifications, but they intend to do it (together with me).
The first task I would like to realize is to explain to some folks
of the company what are the interests of abstraction and specification.

Does anybody there know if I could find some documents describing :

          - Informal specification of a "school-problem" (lifts, coffee-
            machine, ...)

          - Abstract formal specification derived from the previous one
            (with informal comments to explain how the derivation is made)

          - Refinement of the previous specification (pascal-like for instance)


Please, e-mail me ALL the (even small) informations you know about this
kind of work.


			Thanks in advance.

N.B. :

For those who would like a summary of the answers I (hope I)
will receive, just send me an e-mail : I will answer as soon as
I'll have ``enough'' answers.


+--------------------------+------------------------------------+
|                          |    E-mail : charlot@lri.lri.fr     |
|     Francois CHARLOT     |             charlot@FRLRI61.BITNET |
|                          |                                    |
|        +-=-+-=-+         |    Tel    : 33 - 1 - 69 41 70 82   |
|                          |    Fax    : 33 - 1 - 69 41 65 86   |
+--------------------------+------------------------------------+
|      ######      **                                           |
|     ##     #         Laboratoire de Recherche en Informatique |
|    ##       #   ##   Batiment 490                             |
|   ##       #   ##    Universite de Paris-Sud                  |
|  ##    ####   ##     91405 ORSAY CEDEX                        |
| ######    ## ##      FRANCE                                   |
|######      ###                                                |
+---------------------------------------------------------------+