🚀 go-pugleaf

Dear netters.

Some months and some weeks ago, I sent a request in this newsgroup :
I asked if some of you could give me informations about abstraction and
specification. Particularly, I was asking for ``school'' examples of
program development, with possible formal proofs.

I did receive some answers, and I would like to thank all the folks who
wrote me an answer : it was very kind of them. Actually, I did not really
get all the answers I wanted to have, but I have got a lot of references
I am going to use as starting points.

I also received some mails asking me to send an abstract of the answers
I could receive. That is what I am doing here. I cut off parts of certain
messages uninteresting (I guess) for those who asked me this abstract.
I just left the e-mail address of the people who answered, and I hope
they will not mind.

As I am French, some of the answers are in French. I think it is not really
necessary to translate them, because the main idea is internationnaly clear.
If you REALLY need to have the translation, be free to contact me.

After reading this, if you think you can give me more informations about
this subject, please : DON'T HESITATE! More I get informations, happier
I am. Thanks in advance.


		Francois


     +--------------------------+------------------------------------+
     |                          |    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                                   |
     |######      ###                                                |
     +---------------------------------------------------------------+


*******************************************************************************


                              First Attempt


*******************************************************************************


From: John J. Kenney <jjk@CS.Stanford.EDU>
Date: Mon, 27 Jul 92 10:35:01 PDT

I have done some abstraction and specification work,
here at Stanford.  My research group has developed a
specification language to extend Ada called Anna.
I have written a technical report on writting 
Anna specifications, and present a methodology of
abstraction to specification using the abstract
data type Set.

If you are interested I can send you the exact tech
report number and information on how you can order
one.  

John


*******************************************************************************


From: horning@src.dec.com
Date: Mon, 27 Jul 92 11:23:48 -0700

If you have not already seen it, I suggest that you read the book 
"Abstraction and Specification in Program Development," Barabara 
Liskov and John Guttag, 1986, ISBN 0-262-12112-3 (MIT Press), 
0-07-037777996-3 (McGraw-Hill).  This uses only informal specifications, 
but is a good starting point.

Later this year, we hope to announce a new book "Larch: Languages 
and Tools for Formal Specification," John Guttag and James Horning 
(eds.).

You will probably be hearing directly from the Z and VDM communities.
Both Z and VDM have been used for several applications.  If you don't 
get a helpful response on Z, try comp.specification.Z.

I attach a bibliography on Larch, which contains some (relatively 
small) case studies.

Jim H. 

                            Larch References

1. Papers about Larch

1.1. Larch Languages
    J.V. Guttag, J.J. Horning, and J.M. Wing, "Larch in Five Easy Pieces,"
    DEC/SRC SRC-5, July 1985.  (Largely superseded by SRC-58, SRC-72, and
    SRC-74.)

    J.V. Guttag, J.J. Horning and J.M. Wing,
    "The Larch Family of Specification Languages, IEEE Software,
    September 1985, pp. 24-36.  [Also Piece I of SRC-5]

    J.J. Horning
    "Combining Algebraic and Predicative Specifications in Larch"
    Springer-Verlag Lecture Notes in Computer Science 186
    Proc. TAPSOFT, Berlin, Mar. 1985, pp. 12-26.

  Larch Shared Language in particular

    J.V. Guttag, J.J. Horning, and A. Modet, "Report on the Larch
    Shared Language: Version 2.3,"  DEC/SRC SRC-58, April 1990.
    [Supersedes Pieces II and III of SRC-5]

  Larch Interface Languages in particular

    J.M. Wing, "Writing Larch Interface Language Specifications,"
    ACM TOPLAS, January 1987, pp. 1-24. [Also Piece V of SRC-5]

    J.M. Wing, "A Two-Tiered Approach to Sprcifying Programs,"
    Ph.D. Thesis, Laboratory for Computer Science, Massachusetts
    Institute of Technology, May 1983, Report MIT/LCS TR-299.

    D. Guaspari, C. Marceau, and W. Polak, "Formal Verification of Ada
    Programs," IEEE TSE, Vol. 16, No. 9, September 1990, pp. 1058-1075.
 
    J. Chen, "The Larch/Generic Interface Language," MIT S.B. Thesis,
    May 1989.

    R.A. Lerner, "Specifying Concurrent Program Modules,"
    CMU Ph.D. thesis, 1991.
  
    K. Jones
    "LM3: A Larch Interface Language for Modula-3"
    DEC/SRC SRC-72, June 10, 1991.

    J.V. Guttag and J.J. Horning
    "Introduction to LCL, A Larch/C Interface Language"
    DEC/SRC SRC-74, July 24, 1991.

1.2. Larch Tools

  Larch Prover
    S.J. Garland and J.V. Guttag, "An Overview of LP, The Larch Prover,"
    Proc. 3rd Intl. Conf. Rewriting Techniques and Applications,
    LNCS 355, 1989, pp. 137-151.

    S.J. Garland, J.V. Guttag, and J.J. Horning, "Debugging Larch Shared
    Language Specifications," IEEE TSE, Vol. 16, No. 9, pp. 1044-1057.
    [Revised and expanded version of S.J. Garland and J.V. Guttag
    "Using LP to Debug Specifications"
    Elsevier, Proc. IFIP TC-2 WC on Programming Concepts and Methods,
    Tiberias, Mar. 1990.]


  Old
    J.V. Guttag and J.J. Horning, "Report on the Larch Shared Language,"
    Science of Computer Programming, Vol. 6, 1986.  [Pieces II and III
of SRC-5]
 
    J.V. Guttag and J.J. Horning, "A Larch Shared Language Handbook,"
    Science of Computer Programming, Vol. 6, 1986.  [Piece IV of SRC-5]
 
    J.V. Guttag and J.J. Horning
    "An Introduction to the Larch Shared Language"
    Proc. IFIP 9th World Computer Conf., Paris, Sept. 1983, pp.
809-814.

2. Case Studies, Examples

2.1 Specifications written in Larch

  Synchronization Primitives
    A.D. Birrell, J.V. Guttag, J.J. Horning, R. Levin
    "Synchronization Primitives for a Multiprocessor: A Formal Specification"
    OPERATING SYSTEMS REVIEW v. 21, no. 5,
    Proc. 11th SOSP, Austin, Nov. 1987, pp. 94-102.
    [Also published as DEC/SRC SRC-20, Aug. 1987]
    [Revision included in G. Nelson (ed.) "System Programming in Modula-3"
    Prentice-Hall, Mar. 1991.]

  Display
    J.V. Guttag and J.J. Horning, "Formal Specification as a Design Tool,"
    Seventh Symposium on Principles of Programming Languages,
    Las Vegas, Nevada, January 1980, pp. 251-261.

  Larch Handbook
    J.V. Guttag, J.J. Horning, and J.M. Wing, "Larch in Five Easy Pieces,"
    DEC/SRC SRC-5, July 1985.  [obsolete]

  Library example
    J.M. Wing, "A Larch Specification of the Library Problem,"
    Proceedings of the Fourth International Workshop on Software
    Specification and Design, Monterey, CA, April 1987, pp. 34-41.

  Larch/Ada example
    D. Guaspari, C. Marceau, and W. Polak, "Formal Verification of Ada
    Programs," IEEE TSE, Vol. 16, No. 9, September 1990, pp. 1058-1075.

  Larch/Ada example
    S.R. Cardenas and H. Oktaba, "Formal Specification in Larch
    Case Study: Text Manager Interface Specification, Implementation,
    in Ada and Validation of Implementation," Technical Report No. 511,
    Instituto de Investigaciones en Matematicas Aplicadas y en Sistemas,
    Universidad Nacional Autonoma de Mexico, 1988.

  Apple MAC Toolbox
    C.T. Burton, S.J. Cook, S. Gikas, J.R. Rowson, and S.T. Sommerville,
    "Specifying the Apple Macintosh Toolbox Event Manager," Formal
    Aspects of Computing, Vol. 1, No. 2, April-June 1989, pp. 147-171.
 
  Finite element analysis library
    J.W. Baugh, Jr., "Formal Specification of Engineering Analysis
    Programs," The Second International Conference on Expert Systems for
    Numerical Computing, West Lafayette, IN,  April 1990

    J.W. Baugh, Jr. and D.R. Rehak, "Computational Abstractions for
    Finite Element Programming," CMU Civil Engineering TR R-89-182,
    September 1989.

  Avalon built-in classes
    J.M. Wing, "Using Larch to Specify Avalon/C++ Objects,"
    IEEE TSE, Vol. 16, No. 9, September 1990, pp. 1076-1088.

  Avalon examples (atomic queue, directory, counter)
    R.A. Lerner, "Specifying Concurrent Program Modules,"
    CMU Ph.D. thesis, 1991.

  Miro languages and editor
    J.M. Wing and A. Moormann Zaremski, "A Formal Specification
    of a Visual Language Editor," Sixth International Workshop
    on Software Specification and Design, October 1991, Como, Italy,
    submitted January 1991.

  Persistent garbage collection
    S.M. Nettles, "A Larch Specification of Garbage Collection Algorithms,"
    CMU School of Computer Science TR, 1991, in progress.   

2.2. Proofs using LP

  Circuit examples
    S. J. Garland, J. V. Guttag, and J. Staunstrup, "Verification of VLSI
    Circuits using LP," Proceedings of the IFIP WG 10.2, The Fusion
    of Hardware Design and Verification, North Holland, 1988.

    J. Staunstrup, S. J. Garland, and J. V. Guttag, Localized
    Verification of Circuit Descriptions," Proceedings of a Workshop
    on Automatic Verification Methods for Finite State Systems, Grenoble,
    France, June 1989, Lecture Notes in Computer Science, Springer-Verlag.

    J. Saxe et al. SRC-??

  Mathematical Theorems
    U. Martin and T. Nipkow, "Automating Squiggol," Proceedings
    of the Programming Concepts and Methods IFIP TC2 Working Conference,
    Sea of Galilee, Israel, April 1990, pp. 223-236.
 
  Avalon queue example
    J.M. Wing and C. Gong, Experience with the Larch Prover,
    in Proceedings of the ACM Workshop on Formal Methods in
    Software Development," Napa, CA, May 9-11, 1990, pages 140-143.

    C. Gong and J.M. Wing, "Raw Code, Specification, and Proof of
    the Avalon Queue Example," CMU-CS-89-172, August 1989

    J.M. Wing and C. Gong, "Machine-Assisted Proofs of Properties
    of Avalon Programs," CMU-CS-89-171, August 1989.


*******************************************************************************


From: lupus@cs.uni-sb.de (Markus Wolf)
Date: Tue, 28 Jul 92 09:27:40 +0200

Dear Francois,

there is a german research project, called KORSO (german acronym for
correct software) which is especially devoted to software specification
and verification. Our department is working in a subgroup of KORSO 
investigating case studies of software specification. For this reason
we have a small database of specification case studies which you can
ftp from:
		cs.uni-sb.de

The database contains short description of the case studies (unfortunately
in German) and references to the articles (which are fortunately mostly 
english articles). The database consists of single files and can be found
in the directory:

	/pub/obscure/korso/FALLBEISPIELE

I can also send them by mail, if you do not have access to ftp. If you need
more information, please tell me.

	Cheers,

		Markus Wolf


*******************************************************************************


From: Pack.Heng@irisa.fr (Pack Heng)
Date: Tue, 28 Jul 1992 09:50:34 +0200

Hello,

Voici quelques papiers qui devraient te sastifaire :

	L. Lamport, "A Simple Approach to Specify Concurrent Systems",
	Comm. of ACM, Vol. 32, No. 1, Jan. 1989, pp. 32-45.
	(Presentation d'une methodologie de  specification et de verification
	 formelle des programmes concurrents - avec un exemple non pas
	 de machine a cafe mais a boisson).


	K. M. Chandy and J. Misra, "Parallel Program Design, A Foundation",
	Addison-Wesly Publishing Company, 1988.
	(Presentation d'une methodologie de specification, UNITY, simple 
	et claire, accompagnee d'un systeme de preuves pour prouver la 
	correction des raffinements de specification. Le livre montre un
	exemple de specification et de raffinements d'un probleme classique,
	 les philosophes, interessant et instructif ; il contient egalement 
	d'autres exemples).

	M. K. Staskauskas, "The Formal Specification and Design of a Distributed 
	Electronic Funds-Transfer System", IEEE Trans. on computers, Vol. 37, 
	No. 12, Dec. 1988.
	(Specification et raffinement d'un systeme consequent, avec UNITY).


*******************************************************************************


From: "John Haxby (Definitively Wrong -- 830-4558)" <jch@wessex.uucp>
Date: Tue, 28 Jul 92 09:46:44 +0100

Francois,

As a starting point, get hold of this and read it:

	"Abstraction and Specification
	 in Program Development"

	Barbara Liskov and John Guttag

	MIT Press/McGraw-Hill

	ISBN 0-262012113-3 (MIT Press)
	ISBN 0-07-037996-3 (McGraw-Hill)

If you're interested in following up the references to CLU or Larch
I can pass on the ftp sites for compilers and documentation and such.
Contrary to the book, CLU is available on a wider variety of platforms
thanks to the portable CLU compiler.


*******************************************************************************


From: Andreas Spichiger <spchgr@iam.unibe.ch>
Date: Tue, 28 Jul 1992 11:09:55 +0200

I have seen your request in comp.specification. Perhaps I can give you
some help, it depends what you are really looking for:

Our group works in the context of the specification of telecommunication 
systems. We are using the specification languages standardized by CCITT and 
ISO: SDL, Estelle and LOTOS and especially MSC (Message Sequence Charts). If 
you're looking for specifying telecommunication systems or any other 
concurrent procceses, we could have some material for you.

Lifts are also an example we've worked on here quite a lot, since our students 
do it every year. A lift has been specified with Petri Nets. A tool we have 
allows to generate OCCAM-Source from Petri Nets. So it can be run on 
transputer systems.

In my diploma thesis I've used a Routing System described with CSP,
which was also implemented using OCCAM.

I've heard of a lot of work done with Z but am not so familiar with it.

and so on


If you would like to hear more please contact me.

Yours,

Andreas Spichiger


*******************************************************************************


From: Narendra Ravi <naren@cs.ualberta.ca>
Date: 	Tue, 28 Jul 1992 15:03:32 +0100

In comp.specification you write:

   --- text deleted ---

The number of general references to this type of work are too many to list.
I would suggest you try to look at a few examples done in books and papers.

   --- text deleted ---

1. A CSP solution to a simple coffee-machine problem is in Hoare's CSP book.
2. In _Software Engineering Mathematics_, a book authored by Jim Woodcock
   there is a good specification of a telephone system. This also addresses
   the aspect of specification refinement.
3. Specification Case Studies: I. Hayes is also a good reference. In this
   book there are a few specifications, including one on CICS.
4. The fourth International Workshop on Software Specification and Design
   introduces the lift problem and a number of papers present solutions to
   it.
5. Cliff Jones and another person wrote a book on a number of case studies
   in specification using VDM.  See the VDM conferences.
6. Partsch and his group are doing a lot of work in Netherlands. There is a
   recent book by him on Algebraic Specification and Refinement.

   --- text deleted ---

Oh yes, a lot of information exists. Some of the work has been done by the
Oxford Programming Research Group. A lot of work is being done on formal
specifications. Most of the work is in Europe. The best places for such
work in North America are CMU and Univ. of Calif. Irvine.

 -- Naren


*******************************************************************************


From: Michal.Walicki@ii.uib.no
Date: Tue, 28 Jul 1992 18:19:29 +0200

Hi,
I cannot give you anything specific but a reference. A group of people at
Stanford has spent some years developing ANNA - spec. language which is
integrated into Ada. Eventually they got very close to earth, developed
many tools and specified a lot of software. They had a lot of examples and
I guess some of them must have been written down and tested. You can try
and ask Doug Bryan for more information:

        bryan@anna.stanford.edu

        Michal


*******************************************************************************


From: xexeo@dxlaa.cern.ch (Geraldo Xexeo)
Date: Tue, 28 Jul 92 19:30:20 +0200

Try to have a look in the book:

Pratical Formal Methods with VDM

  Derek Andrews and Darrel Ince
  McGraw Hill International Series in Soft. Eng.

It has the informal/formal specification part of a text editor.

And in the paper:

 An introduction to > and formal specifications

  J.M. Spivey

  Software Engineering Journal 1989

  where the 3 phases are done for a birthday book (text/Z/Pascal).


       Cheers,

			Jerry


*******************************************************************************


From: jmichael@gmuvax2.gmu.edu (James Bret Michael)
Date: Tue, 28 Jul 92 19:56:08 -0400

I will mail you a copy of a presentation I attended on the
use of formal methods for specifying safety-critical systems.
The material has names and addresses of people you can
contact for additional information.

   --- text deleted ---

A bientot

Bret


*******************************************************************************


From: mann@anna.Stanford.EDU (Walter Mann)
Date: Wed, 29 Jul 1992 13:37:41 -0700

Doug Bryan has forwarded your request to me for information on Anna
and formal specifications.  We have a fairly large set of example Ada
packages which have been formally specified in Anna.  Many of them are
simply different abstract data types, but there are some larger
examples also.  This set of examples is available as a Technical
Report from Stanford University, but I will simply mail you a copy if
you'd like.  Just to double-check, your mailing address is:

   --- text deleted ---

Also, in case you'd like more information on Anna itself, I've
included our introductory document below.  Let me know if you have any
further questions.

Walt Mann
Stanford Anna Group

---------------------------------------------------------------------
Thank you for your interest in Anna and the Anna toolset.  This
document introduces the language and the current tool status and
availability.  If you have any further questions, please don't
hesitate to contact us at the addresses given in the "Support" section
of this document.


               Information on Anna and the Anna Tools
               --------------------------------------

Introduction
------------

Anna is a language extension of Ada to include facilities for formally
specifying the intended behavior of Ada programs.  It is designed to
meet a perceived need to augment Ada with precise machine-processable
annotations so that well-established formal methods of specification
and documentation can be applied to Ada programs.


Language
--------

The Anna language is described in many documents.  There are two
readily available sources of information on the language.  One is the
Springer-Verlag Anna Reference Manual, volume 260 of the Lecture Notes
in Computer Science series.  The primary author is David C. Luckham.
This manual may be purchased at any computer bookstore, and is
probably available in any mathematical reference library.

An introductory text on using Anna is available now, published by
Springer Verlag in their _Silver series_, Texts and Monographs in
Computer Science.  The title of this book is _Programming with
Specifications: An Introduction to ANNA, A Language for Specifying Ada
Programs_, by David C. Luckham.

Various aspects of the Anna language and Anna tools have been
documented in technical reports and published papers.  See the
bibliography for a complete list of applicable documents.


Anna Tools
----------

The Program and Analysis Group at Stanford University has developed a
prototype environment supporting the Anna language.  The first release
of this environment, Anna-I, is available to anyone who wishes to
experiment with it.  The tools implement a large subset of the Ada and
Anna languages.  These tools include:

	-- Intermediate Representation Toolkit (Extended DIANA Formal
           Interface and Implementation packages (AST), Ada/Anna
           Parser, Ada/Anna Pretty Printer, AST Disk <==> Memory
           package)
	-- Ada/Anna Static-Semantic Rules Checker
	-- Annotation Transformer
	-- Portable Ada/Anna Testing and Debugging System
	-- Ada/Anna AST Browser
	-- Ada Logic Reasoning System (a PROLOG interface)
	-- Anna Package Specification Analyzer
	-- Anna Interactive Tutorial System

The Anna-I tools are completely implemented in Ada, though a small
amount of X-Windows and Verdix VADS dependency exist in some of the
user-interfaces.

The AST IR interface defines the common internal representation used
by all the Anna-I tools---routines are exported that allow traversal
and data manipulation of an AST.  The Parser parses Anna text files
into the AST representation.  The Pretty Printer generates ASCII text
given an AST.  The AST Disk <==> Memory package performs AST
disk-to-memory conversions, and vice versa.

The Semantic Checker checks the static-semantics of the Ada and Anna
code in the AST: it works in both batch and incremental modes.

The Annotation Transformer maps an Anna program to an equivalent Ada
program.  That is, the Transformer replaces Anna constructs with Ada
checking constructs in order to build a self-checking program.  The
Testing and Debugging system can then be used to monitor the run-time
behavior of the transformed program.  Currently, the Testing and
Debugging system is provided with a small, command-line interface, and
for some releases, an X-Windows and Emacs editor interface.

The AST Browser is an X-Windows based tool for graphically traversing
and examining an Anna AST.

The Ada Logic system is an Ada package which is an interface to a
Prolog interpreter.  It allows the user to build clauses and databases
of knowledge, and make queries with respect to the databases.

The Specification Analyzer is an interactive tool for examining and
debugging the visible part of an Ada/Anna package specification using
deduction and symbolic execution.

The Anna Interactive Teaching Tutorial is an interactive tutorial for
Anna.  It is designed to familiarize the user with basic Anna concepts
and language facilities.  Several ``hands-on'' exercises are included.
Anna Teach automatically invokes other Anna tools and the Ada compiler
to check the correctness of exercises entered by the user.

We are currently developing other Anna-I tools that include:

	-- Parallel Testing and Debugging System (for Sequent
           Symmetry) 
	-- more robust incremental semantics capabilities for Ada and Anna 


FTP Availability
----------------

Anonymous FTP for the Anna-I environment and various Anna papers are
available on the Internet host ``anna.stanford.edu'' [36.14.0.13].
The file ``pub/anna/read.me'' in this FTP account has more details;
please read this document before transferring any other files.

Also, if you do acquire the Anna tools via FTP, please let us know; we
like to keep track of who is using the tools, and how.


Acquiring the Anna-I Tools
--------------------------

If the FTP acquisition method is not a viable option, you may obtain
an Anna-I release through postal mail.

The Anna-I release requires two 9-track, 1600-bpi magnetic tapes (one
for the Anna-I tools and one for the X-Windows interface used by the
Anna-I tools).  It includes an installation guide and user's manual.
To obtain an Anna-I release, please send us tapes and a
self-addressed, stamped, return package with applicable postage to:

	Stanford Anna Team 
	Computer Systems Lab, ERL 456 
	Stanford University 
	Stanford, CA  94305

NOTE: Include enough postage to cover the cost of sending the magnetic
tape(s) plus a 75 page document.

Most of the Anna tools rely on the use of the Verdix VADS compiler.
We do not have source code for any other compiler.  However, we are
available to answer any questions you might have about porting the
Anna-I toolset.

If you would like a pre-compiled release of the Anna-I tools, we have
releases available for the following systems:
	-- Sun/3 UNIX version 4.0.3, Verdix VADS 6.0.3(c) Ada compiler
	-- Sequent Symmetry DYNIX (i386), SLI/Verdix VADS 5.5.2 Ada
           compiler 

Due to the considerable time and resources required to produce a
pre-compiled Anna-I release, as well as the limited hardware we have,
we are only currently able to produce pre-compiled releases in these
two formats.  We do not have a Sun/3 cartridge drive readily
available.  We do not have a VAX/VMS system so we cannot provide any
VAX/VMS tape format pre-compiled release of the Anna-I tools.

Please inform us which version of the Anna-I tools you would like
(Sun/3 OS 4.0.3 with Verdix VADS 6.0.3(c), or Sequent Symmetry DYNIX
SLI/VADS 5.5.2).  If you have any questions, contact the Stanford Anna
Team.


Support
-------

Support for learning Anna and the tool set is very limited.  A short
one-day tutorial course will soon be available at a fee.  Contact us
for details regarding Anna language and tools support.

An Anna User's Group is now being supported through Internet
electronic mail.  Announcements of new releases, new tools, bug fixes,
etc. will be posted through this medium.  To obtain information about
being added to the list, please contact us as the following address,
phone, or electronic mail:

	Stanford Anna Team 
	Computer Systems Lab, ERL 456 
	Stanford University 
	Stanford, CA  94305

	(415) 723-1175 (voice) 
	(415) 725-7398 (fax) 
	anna-request@anna.stanford.edu


Bibliography
------------

_Reference Manual for the Ada Programming Language_.
U. S. Department of Defense, U. S. Government Printing Office,
  ANSI/MIL-STD-1815A edition, January 1983.

Douglas L. Bryan and Geoffrey O. Mendal.
_Exploring Ada, Volume 1_.
Prentice-Hall, Englewood Cliffs, New Jersey, 1989.

G. Goos, W. A. Wulf, A. Evans Jr., and K. J. Butler.
_DIANA, An Intermediate Language for Ada_.
Volume 161 of _Lecture Notes in Computer Science_,
  Springer-Verlag, 1983.

D.C. Luckham, Randall Neff, and David Rosenblum.
_An Environment for Ada Software Development Based on Formal
  Specification_.
Technical Report CSL-TR-86-305, Stanford University, August 1986.
Also published as an article in Ada Letters, VII(3):94--106,
  May/June 1987.

David Luckham, Sriram Sankar, and Shuzo Takahashi.
_Two Dimensional Pinpointing: An Application of Formal
  Specification to Debugging Packages_.
Technical Report CSL-TR-89-379, Stanford University, April 1989.
Also published as an article in IEEE Software, 8(1):74--84,
  January 1991.

David C. Luckham.
_Programming with Specifications: An Introduction to ANNA,
  A Language for Specifying Ada Programs_.
_Texts and Monographs in Computer Science_, Springer-Verlag,
  October 1990, 412 pages.

David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brueckner, and Olaf
  Owe.
_ANNA, A Language for Annotating Ada Programs_.
Volume 260 of _Lecture Notes in Computer Science_, Springer-Verlag,
  1987.

Geoffrey O. Mendal.
Designing for Ada reuse: A case study.
In _IEEE Computer Society Second International Conference on Ada
  Applications and Environments_, pages 33--42, IEEE Computer Society, Miami
  Beach, Florida, 8-10 April 1986.
Also published as a Stanford University Technical Report, June 1986,
  CSL-86-299.

Geoffrey O. Mendal.
_The Anna-I User's Guide and Installation Manual_.
Stanford University, Computer Systems Lab, ERL 456, Stanford, California,
  version 1.3 edition, May 1991.

Randall Neff.
_Ada/Anna Specification Analysis_.
PhD thesis, Stanford University, Stanford, California, December 1989.
Also published as a Stanford University technical report, CSL-TR-89-406.

David S. Rosenblum.
_A Methodology for the Design of Ada Transformation Tools in a
  DIANA Environment_.
Technical Report 85-269, Stanford University, February 1985.
Also published in IEEE Software, 2(2):24--33, March 1985.

David Rosenblum, Sriram Sankar, and David C. Luckham.
_Concurrent Runtime Checking of Annotated Ada Programs_.
Technical Report CSL-TR-86-312, Stanford University, November 1986.
Also published in the _Proceedings of the 6th Conference on
  Foundations of Software Technology and Theoretical Computer
  Science_, Volume 241 of _Lecture Notes in Computer Science_,
  Springer-Verlag, 1986.

Sriram Sankar.
_Automatic Runtime Consistency Checking and Debugging of Formally
  Specified Programs_.
PhD thesis, Stanford University, Stanford, California, July 1989.
Also published as a Stanford University Technical Report, August 1989,
  CSL-TR-89-391.

Sriram Sankar and David Rosenblum.
_The Complete Transformation Methodology for Sequential Runtime
  Checking of An Anna Subset_.
Technical Report CSL-86-301, Stanford University, June 1986.


*******************************************************************************


From: S.P.vandeBurgt@research.ptt.nl (Stan P. van de Burgt)
Date: Thu, 30 Jul 92 10:18:06 +0200

In comp.specification you write:

   --- text deleted ---

Some case studies were performed in some European Committee projects.
The ones I can think of right now are:

- SPECS (Specification and Programming Environment for Communication Software)
  [RACE Ref 1046.]

- Lotosphere [Esprit 2304]

You might try the following addresses in France:

SPECS:
            Philippe Deysine
            Project Manager
            GSI - Tecsi
            6 cours Michelet
            92064 PARIS LA DEFENSE Cedex 52
            email: specs@gsitecsi.UUCP


Lotosphere:
            Pierre Azema
            LAAS du CNRS
            7 Avenue du Colonel Roche
            31077 Toulouse cedex
            email: azema@laas.laas.fr

            Elie Najm
            INRIA/Rocquencourt
            Domaine de Voluceau
            BP 105
            78153 LE CHESNAY CEDEX
            email: najm@nuri.inria.fr

--
   S.P. van de Burgt


*******************************************************************************


From: Andreas Spichiger <spchgr@iam.unibe.ch>
Date: Mon, 3 Aug 1992 17:11:45 +0200

Concerning your interest in lift specifications and so on:

can you handle / read german documentation? Since we are in the german part of 
Switzerland, almost all documentation of students projects are done in german.

Yours,

Andreas Spichiger


*******************************************************************************


From: sankar@mycroft.Stanford.EDU (Sriram Sankar)
Date: Tue, 4 Aug 92 09:39:59 PDT

Hi Francois,

Doug Bryan forwarded to me your message requesting for specification
examples.  I'm sure others in our group will have responded by now,
however, I recommend that you look at an article that we authored and
appeared in the Jan.1991 issue of IEEE Software.  It is titled:
"Two-dimensional pinpointing ... ".

This article talks about how one can debug a formally specified program.
I can also mail to you a technical report containing a lot of small
examples specified using Anna - authored by Walter Mann and John Kenney.
Maybe you have already communicated with Walter and he has already sent
you that report.

Please let me know if you need any more help.

Sriram.


*******************************************************************************


From: George Loegel <ettare@dip.eecs.umich.edu>
Date:  Tue, 4 Aug 1992 14:15:34 -0500

Greetings,
  This is also an area I'm working in for my Ph.D. thesis. I mostly
working with algebras to specify systems and then use the algebras to
develop the system.  
  Two works might be of interest:

   1. Algebraic Specification in Software Engineering by Ivo Van
Horebeek and Johan Lewi Springer-Verlag 1989 
   2. A Unifying Framework for Structured Analysis and Design Models
by T. H. Tse, Cambridge University Press 1991

I would naturally be curious about your plans.

Good Luck! 

George J. Loegel


*******************************************************************************


From: Pierre Azema <azema@droopy.laas.fr>
Date: Wed, 5 Aug 92 10:16:13 +0200

Le projet LOTOSPHERE a produit LITE: Lotos Integrated Tool Environment
	qui est disponible a tous, par exemple via le LAAS,

Pour avoir une demo: passer au LAAS, (ou en region Paris voir E.Najm)


Pour apprendre a s'en servir:
	third LotoSphere Workshop, Pise 14-16 Sept 92
	contacter  bolog@fdt.CNUCE.CNR.IT 


	
	WORKSHOP - FIRST DAY

8:30	Registration
9:00	Welcome

--------------------------------------------------------------
INTRODUCTORY PRESENTATIONS AND OVERVIEWS
(Chair: C. A. Vissers)


9:10	C. A. Vissers***, L. Ferreira Pires, J. v.d. Lagemaat
	LotoSphere, an attempt towards a Design Culture 
	
9:40	E. Brinksma***
	The LOTOS language (paper?)

10:20	J. Quemada***, A. Azcorra, S. Pavon 
	Development with LOTOS
	
11:00	====== break ======
	
11:20	J. Manas***
	Getting to Use LITE (with demo)
	
12:20	E. Wiedmer***
	LOTOS industrial applications
		
13:00	====== lunch ======

	
--------------------------------------------------------------
DEVELOPMENT TRAJECTORIES FOR INDUSTRIAL APPLICATIONS 
(Chair: J. Quemada)


14:00	K. Turner***, M. van Sinderen
	LOTOS specification style for OSI
		
14:40	H. Eertink***
	Executing LOTOS specifications: the SMILE tool (with demo)

15:20	A. Azcorra***, J. Quemada, J. Manas
	A pragmatic approach to verification, validation and compilation
	(with demo)
	
16:00	====== break ======

16:20	J. P. Courtiat***, D. E. Saidouni
	A case study in protocol design


------------------------------------------------------------
SHORT PRESENTATIONS OF FURTHER, OFF-LINE TOOL DEMOS 
(Chair: J. de Meer) 


17:00	C. Wezeman***
	Deriving tests from LOTOS specifications
	(tool COOPER)
	
17:30	D. Wolz***
	A tool for checking ADT completeness and consistency

18:00	end
	
	
	
============================================================
20:00	Cocktail party
============================================================



	WORKSHOP - SECOND DAY
	
------------------------------------------------------------
INNOVATION IN THE DESIGN TRAJECTORY 
(Chair: T. Bolognesi)


9:00	T. Bolognesi, D. De Frutos, R. Langerak***, D. Latella
	Correctness Preserving Transformations for the 
	early phases of software development

9:30	P. Cunha, A. Fantechi, B. Mekhanet, E. Najm***(?) 
	Correctness Preserving Transformations for the 
	late phases of software development

10:00	E. Madelaine***
	An exercise in protocol verification (with demo)
	
10:30	L. Ferreira Pires, J. Schot***
	Design and implementation strategies
	
11:00	====== break ======


--------------------------------------------------------------------
SHORT PRESENTATIONS OF FURTHER, OFF-LINE TOOL DEMOS 
(Chair: A. Fantechi) 


11:30	A. Lakas, E. Najm***
	ALTO: An interactive transformation tool
	
12:00	E. Dubuis, K. Warkentyne  (?***)
	The COLOS compiler
		
12:30	====== lunch ======


-----------------------------------------------------------	
APPLICATIONS 
(Chair: R. Booth)


14:00	R. Booth*** 
	Applying LOTOS to OSI Application Layer Protocols (paper?)
	
14:30	V. Jones***
	Realization of CCR in C

15:00	G.-J. van der Heijden, I. Widya***, F. Juillot
	TP Protocol from Specification to Implementation
	
15:30	K. Warkentyne*** (to be checked)
	<paper on Mini-Mail application> ?
	
16:00	====== break ======

	
-----------------------------------------------------------
LOTOS ENHANCEMENTS 
(Chair: E. Brinksma)


16:20	E. Brinksma, G. Leih***
	Enhancements of LOTOS

16:50	R. Roth***
	Data Type Specifications in Modular LOTOS (paper?)
	
17:20	end
	





	SEMINAR - THIRD DAY
	
-----------------------------------------------------------
THE LOTOS INTEGRATED TOOL ENVIRONMENT
Coordinated by J. Manas


E. Madelaine			Verification, visualization
H. Eertink			Simulation
A. Azcorra			Validation/Testing
J. Manas			Compilation
E. Salvatori, M. Caneve		Editing and static analysis


 8:45	J. Manas	
	Introduction to the day

 9:00	First parallel session		
10:00	Second parallel session

11:00	====== Break ======

11:30	Third parallel session

12:30	====== Lunch ======

14:00	Fourth parallel session
15:00	Fifth parallel session

16:00	====== Break ======

16:30	Closing Session - discussion.

17:30	end


*******************************************************************************


From: aguilla%agt.uucp@cs.ualberta.ca
Date: 	Tue, 11 Aug 1992 13:07:38 +0100

Just read your note on the Net.

To me, informal specifications are just that. A document listing in a
language
(english or French whatever) what the customer wants. Of course, the
customer
generally is not able to write exactly what is needed in a precise manner
suitable for mechanization. The analyst must then go to work and make the
specification formal (that is able to be executed). This task often
involves
many meetings with the customer clearing up whatever was not clear and
specific
enough. 

Knowledge representation is the science of formalizing an initial informal 
specification. One needs a model and method, which depends on what the
customer
wants to do and the knowledge of the analyst. At first a very manual
activity,
slowly becoming more automatic until the job is finished.

>From what you wrote, it seems that you are trying to find a way to write
down
the specification in such a manner that automating becomes very easy. That
is
formalizing the specification already. 

As any software development must go through the development steps, you
should
have no problem obtaining examples from the company! Perhaps they want you
to
find out a better model or methodology than what they have been using. If
that is
the case the Comuting Science department should be able to help you.

In any case, have lots of fun!

August Guillaume


*******************************************************************************


                              Second Attempt


*******************************************************************************


From: mjl@cs.rit.edu (Michael J Lutz)
Date: Tue, 15 Sep 92 15:44:10 EDT

In article <1992Sep15.110521@sun3.lri.fr>, you write:

   --- text deleted ---

Most of the work I've done is in Z (Oxford PRG), so my references wil
reflect that.

1. Get Spivey's Z Reference Manual 2nd Edition (Prentice-Hall, 1992).
It starts with a simple example of a system to maintain a list of
persons and their birthdays.  From this simple base, Spivey does the
following:
	a. Shows how to use Z's schema calculus to turn partial operations
	   into total operations (precondition = true).
	b. Shows how to refine the abstract specification into a design
	   that translates directly into Pascal (well, almost Pascal).

He also specifies a checkpoint/restart scheme for a database system
and then breaks down one of the operations into two simpler ones
that can be composed sequentially.

2. The book Specification Case Studies by Ian Hayes (Prentice Hall, 1988)
has several case studies in Z.  Unfortunately, the language has evolved
since the book was published, but word is that a 2nd edition which conforms
to Spivey's book above should be out Real Soon Now.

3. Look at the text An Introduction to Formal Specification and Z by
Potter, Till, and Sinclair (Prentice Hall, 1992).  There are a couple of
simple examples worked out there as well.

4. Finally, see if you can acquire The Theory and Practice of Refinement:
Approaches to the Formal Development of Large-Scale Software Systems.
(edited by John McDermid, Butterworths, 1989).  This has several case
studies, including one for the ``classic'' library problem from Steve
King and Ib Sorensen in Z.  In this case, they specify the whole system,
then refine part of it to a design and finally they ``implement'' part
in Dijkstra's guarded command language.   The one problem with this book
is that it apparently costs the gross domestic product of a small nation
to purchase (something like $130 in the US, where most books its size would
go for $25 to $35).

Hope this helps.  If you need more, please feel free to send me a note.

-- 

Mike Lutz


*******************************************************************************


From: vutien@geant.cenatls.cena.dgac.fr (Vu Tien)
Date: Wed, 16 Sep 92 09:24:21 +0200

   --- text deleted ---

Je crois que Bertrand Meyer a ecrit il y a quelque temps de cela un article
pour decrire sa methode M

L'article fait 30 pages (!) et decrit une implementation d'un driver de disque
avec traduction en Eiffel (d'apres mes souvenirs).

vutien.


*******************************************************************************


From: JON@gaffer.radonc.washington.edu (Jon Jacky)
Date:    Wed, 16 Sep 1992 9:25:35 -0700 (PDT)

Francois Charlot:

Regarding your search for case studies ---

   --- text deleted ---

I am concerned with the safety of medical devices that contain or use
computers.  Currently, I am investigating formal approaches to specifying and
developing software for the control system of a medical cyclotron that we use
for neutron radiation therapy and isotope production.  We've written a huge
(hundreds of pages) informal prose specification and I've gotten pretty far
writing Z formalizations of much of it, and thinking how we're going to
implement it.  For some parts I've even done a development from an initial
abstract Z specification to a more concrete Z specification.  It's probably
much too large to use for one of your case studies, though.

Jonathan Jacky				jon@radonc.washington.edu


*******************************************************************************


From: Cliff B Jones <cliff@computer-science.manchester.ac.uk>
Date: 17 Sep 92 07:54:36+0100

RFC-822-HEADERS:
Newsgroups: comp.specification
Organization: Dept Computer Science, University of Manchester, U.K.

You might look in 

@book{Jones80a,
	author =	"C.~B.~Jones",
	title =		"Software Development: A Rigorous Approach",
	publisher =	"Prentice Hall International",
	year =		"1980"
}

For example Chapter 21

cliff jones


*******************************************************************************


From: Marc Frappier <mfrappie@csi.UOttawa.CA>
Date: Fri, 18 Sep 92 09:12:40 -0400

Bonjour Francois.

Je travaille egalement sur le raffinement de specifications a l'Universite
d'Ottawa.  Nous avons comme hypothese que nous disposons d'une specification
formelle.  Nous essayons de developper un ensemble de regles de raffinement
pour transformer une specification en un programme executable.  Nous utilisons
l'algebre relationnelle pour ecrire les specifications et pour definir la
semantique d'un programme.

Il y a beaucoup de gens en intelligence artificielle qui essaient de
formaliser une specification informelle (comprehension du langage naturel,
detection des ambiguites, etc).  Nous avons une autre approche.  Nous estimons
qu'une specification doit etre ecrite initialement dans un langage formel.
Une specification formelle est validee et verifiee pour s'assurer qu'elle
correspond bien aux attentes de l'utilisateur.

Je ne connais pas d'exemple ou une specification informelle est raffinee
jusqu'a obtenir un programme executable.  Toutefois, il en existe plusieurs
dans le cas formel a programme.  Le livre de Carroll Morgan "Programming
from specifications" (Prentice-Hall 1990) est tres bien ecrit.  Egalement,
voici une liste de d'articles de notre groupe de recherche qui pourrait
t'aider.


N. Boudriga, F. Elloumi and A. Mili.  On the Lattice of Specifications: 
	Applications to a Specification Methodology.  To appear in Formal
	Aspects of Computing.

J. Desharnais, A. Jaoua, F. Mili, N. Boudriga and A. Mili. A Relational
	Division Operator: The Conjuguate Kernel.  To appear in Theor.
	Comp. Sci. 113, August 1993.

A, Mili, J. Desharnais and F. Mili.  Relational Heuristics for the Design
	of Deterministic Programs. Acta Inform. 24,3, 1987, pp. 239-276.

F. Mili, A. Mili.  Heuristics for Constructing While Loops.  Sci. Comp. Prog.
	18, 1992, pp. 67-106.

N. Boudriga, A. Mili, R. Zalila and F, Mili.  A Relational Model for the
	Specification of Data Types. Comput. Lang., 17,2,1992, pp. 101-131.

N. Boudriga, A. Mili, R. Zalila.  An Automated Tool for Specification 
	Validation: Design and Preliminary Implementation, in Proc of the
	Hawaii International Conf on System Science. vol 2, 1992.

En esperant que cela puisse t'aider.

Marc Frappier


*******************************************************************************


From: Luiza Carneiro <luiza@csg.uwaterloo.ca>
Date: Mon, 21 Sep 92 16:05:53 EDT

> 
> Hi,
>    I read your message i the news group.
>    I wrote a paper (with a group of people) about formalizing
> CAD for VLSI. Seems complicated, ahm...
> But the actual formal part, in my opinion is fairly simple. 
> Probably would be worth taking a look. It was published in the
> IBM System Journal - vol. 28, no.4 1989. The title is: Garden - an
> evolving ....
> If you have any questions, feel free to ask.
>   Another PhD student :-)
>      Luiza
> 


*******************************************************************************


                              End of 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                                   |
|######      ###                                                |
+---------------------------------------------------------------+