On Wed, 8 Dec 1999, Ian Phillips wrote:
> >can claim credit for Z. I've also never [s]een it outside the classroom.
>
> I seen it in bookstores if that makes you feel better ;-)
Actually, I heard a lecture in August 1998 given by Pamela Zave from AT&T
Labs on how they use Z for modelling feature interaction in
telecommunications software. You can find more information on her homepage
at http://www.research.att.com/info/pamela
A realated specification method is the B method, that was actually used
for designing the braking system of the driverless metro in Paris.
If you want to know more, a good place to start is
http://archive.comlab.ox.ac.uk/formal-methods/b.html
Personally, I don't think formal specification is the solution for every
software project, but it can be (and is, to some extent) used when
developing safety critical software. The main problem with formal
specification is that it needs for the programmer to be familiar with
formal logic, which is not always the case. Once you know formal logic and
its notation, the formal specification is much like making a prototype.
The difference is that you can (usually) both test your prototype and
formally prove that it has wanted properties.
I hope I don't sound like an expert on the subject, because I'm not. I
know Z (I've taken a course) and some of my close friends work with B.
Jeanette
--- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---
Jeanette Heidenberg, MSc | | [EMAIL PROTECTED]
CS at Abo Akademi Uni | Does fuzzy logic tickle? | [EMAIL PROTECTED]
Finland | | www.infa.abo.fi/~jeanette
************
[EMAIL PROTECTED] http://www.linuxchix.org
