Re: Step-by-step instructions to formal specification of a class needed!!

alwalsh@rbg.informatik.th-darmstadt.de (Andreas Walsh) writes:


>I'm part of a group that has about a week to formally specify a class that uses
>Borland C++ container arrays. Our problem is that we haven't decided on which
>specification system to use, mainly because we haven't found any suitable
>descriptions of these systems.

>We have looked in a fair couple of books, but they have been much too long-winded for our purposes.

>What we would like is a quick step-by-step approach to formally specifying a class. (the class has already been implemented in code!)

Quick?  Probably not.

But there is a bit of this in the Larch/C++ reference manual,
chapter 7, in a discussion of the introductory examples.
Also, you may be interested in the Larch/C++ specification of
some of the MFC classes.

All of this is reachable through the URL for Larch/C++.


In fairness, you can also try some of the other formal method tools
geared towards OO.  Look in

<A HREF="http://www.comlab.ox.ac.uk/archive/formal-methods.html">
The World-Wide Web Virtual Library: Formal Methods</A>

for example, you might look at the

<A HREF="http://ruunfs.fys.ruu.nl/FI/afrodite/papers.html">
Afrodite project and VDM++</A>.

Also check out the work of Alan Wills on Fresco...

	Gary Leavens
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html