[Prev][Next][Index]
Re: Step-by-step instructions to formal specification of a class needed!!
alwalsh@rbg.informatik.th-darmstadt.de (Andreas Walsh) writes:
>Hi!
>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++.
http://www.cs.iastate.edu/~leavens/larchc++.html
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
Reference(s):