Re: Step-by-step instructions to formal specification of a class needed!!
firstname.lastname@example.org (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
The World-Wide Web Virtual Library: Formal Methods</A>
for example, you might look at the
Afrodite project and VDM++</A>.
Also check out the work of Alan Wills on Fresco...
229 Atanasoff Hall, Department of Computer Science
Iowa State Univ., Ames, Iowa 50011-1040 USA / email@example.com
phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu