Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!spool.mu.edu!snorkelwacker.mit.edu!bloom-beacon!eru!hagbard!sunic!mcsun!ukc!axion!puppis!pyoung
From: pyoung@axion.bt.co.uk (Pete Young)
Newsgroups: comp.specification
Subject: Re: The best tutorial on formal specifications
Message-ID: <1991May22.085600.21237@axion.bt.co.uk>
Date: 22 May 91 08:56:00 GMT
Article-I.D.: axion.1991May22.085600.21237
References: <1991May21.132856.27452@dcs.glasgow.ac.uk>
Sender: news@axion.bt.co.uk
Reply-To: pyoung@zaphod.axion.bt.co.uk
Organization: British Telecom Research Labs
Lines: 30

From article <1991May21.132856.27452@dcs.glasgow.ac.uk>, by jack@dcs.glasgow.ac.uk (Jack Campin):

> Much of the literature on model-based specification does quite well at
> describing how you start constructing a spec and the tradeoffs involved in
> different factorizations.  I don't know anything as good from the algebraic
> side; does anyone?

One paper that I found useful (especially if the reader is already
familiar with the model-oriented notations, in this case VDM):

Formal Specification -  A comparison of two techniques.
D. A. Duce and E. V. Fielding
The Computer Journal, Vol 30, No 4 1987

This paper compares the two specification styles by specifying a
problem in VDM and OBJ. If you are familiar with one style, it is a useful
tutorial to the other.

Another book containing good examples is the recent one on Z by Potter,
Sinclair and Till, although it does not fit the original criterion since
it is not a tutorial paper. IMHO, I should probably add.

Regards

Pete


  ____________________________________________________________________
  Pete Young         pyoung@axion.bt.co.uk        Phone +44 473 645054
  British  Telecom  Research Labs,  Martlesham Heath   IPSWICH IP5 7RE