🚀 go-pugleaf

Thanks to all who responded to my request about "The  best  tutorial  on
formal  specifications",  for  undergraduates  taking  a first course on
software engineering.  Since there was enough interest,  I'm summarizing
here.

Before getting the responses, my initial candidates where  C.A.R. Hoare,
"An  Overview  of  Some  Formal  Methods  for Program Design", Computer,
September 1987, and articles from September 1990 of both  IEEE  Software
and Computer.  I found some consistency with these responses.

Pablo Straub
straub@cs.umd.edu


------------------------------------------------------------------------
From: xexeo@cernvax.cern.ch (geraldo xexeo)

There are VERY good papers of Z, that  you  can  use  as  tutorials  for
formal  specifications,  in the Software Engineering Journal of Jan. 89.
Specially, there is "An introduction to Z and formal specifications"  by
J. Spivey, which I consider the best I saw until now.
------------------------------------------------------------------------
From: elkassas@eb.ele.tue.nl (sherif el kassas)

The specification of complex systems by B. Cohen, W.T. Harwood and  M.I.
Jackson.  -  Amsterdam  :  Addison-Wesley,  1986.  -  XII, 143 p. - ISBN
0-201-14400-X. A nice introduction. It builds up the argument/motivation
for using formal  methods.  It's  most  important  feature  is  that  it
compares  and  overviews the main approaches to formal methods (i.e. the
process, model, and algebraic approaches).

I would also  suggest  the  following  IEEE  special  issues  on  formal
methods:

- IEEE  Transaction  on  Software  Engineering,  volume  16,  number  9,
  September 1990.

- IEEE Software, September 1990. A must read in this issue: "Seven myths
  of formal methods", by A. Hall, pages 11-19", I think it won the  best
  IEEE paper of 1990.

- IEEE Computer, September 1990.
------------------------------------------------------------------------
From: horning@src.dec.com (Jim Horning)

Look and Jeannette Wing's in (I think) the September 1990 IEEE COMPUTER,
special issue on formal methods.
------------------------------------------------------------------------
From: maa@SEI.CMU.EDU (Mark A. Ardis)

Jeannette Wing's tutorial in 9/90 IEEE Computer is my pick for the
best tutorial paper.
------------------------------------------------------------------------
From: bourd@cps.msu.edu (Robert Bourdeau)

As a motivational paper, how about David Gries paper in CACM a couple of
months ago. "Towards a More Effective Curriculum".  It's  easy  reading,
has  some  thought  provoking  ideas,  and introduces the formal methods
approach.
------------------------------------------------------------------------
From: sergio@cs.umd.edu (Sergio Cardenas)

Mathematics of Programming, C.A.R. Hoare, Byte, August 1986, pp. 115-126.
This may be appropriate to a more general audience.
------------------------------------------------------------------------

straub@cs.umd.edu (Pablo A. Straub) wrote:
> From: elkassas@eb.ele.tue.nl (sherif el kassas)

> The specification of complex systems by B. Cohen, W.T. Harwood and  M.I.
> Jackson.  -  Amsterdam  :  Addison-Wesley,  1986.  -  XII, 143 p. - ISBN
> 0-201-14400-X. A nice introduction. It builds up the argument/motivation
> for using formal  methods.  It's  most  important  feature  is  that  it
> compares  and  overviews the main approaches to formal methods (i.e. the
> process, model, and algebraic approaches).

I didn't like the algebraic section of this book at all.  You get presented
with a very complicated and unusually structured specification in one swell
foop, with no hint as to how the author might have arrived at it.

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?


-- 
--  Jack Campin   Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, Scotland   041 339 8855 x6854 work  041 556 1878 home
JANET: jack@dcs.glasgow.ac.uk   BANG!net: via mcsun and ukc   FAX: 041 330 4913
INTERNET: via nsfnet-relay.ac.uk   BITNET: via UKACRL   UUCP: jack@glasgow.uucp

Some additional "motivational" sources:

[Dijkstra 76-1] E.W.Dijkstra. The teaching of programming, i.e., the teaching of
thinking. In: Lecture Notes in Computer Science, Vol.46. Springer Verlag, 1976.
[Dijkstra 82] E.W.Dijkstra. Selected writings on computing: a personal
perspective. Springer Verlag, 1982.
[Meyer 89] B.Meyer. From structured programming to object-oriented design: the
road to Eiffel. Structured Programming, Vol. 1 (1989), No. 1, pp.19-39.


Hope this helps.

-Haim Kilov
haim@bcr.cc.bellcore.com

An excellent _book_ on formal specifications is:
@BOOK{GM86,
  KEY           = "GM86",
  EDITOR        = "N. Gehani and A.D. McGettrick",
  TITLE         = "Software specification techniques",
  PUBLISHER     = "Addison-wesley publishing company",
  YEAR          = 1986
}

The book brings together 21 important (and by now sometimes "classical")
articles on (formal) specification. The articles are grouped in four sections,
each of which considers a particular aspect of the subject.
The book is from 1986, so _very_ recent articles are not covered.



(I got the tip quite a while ago from this newsgroup as well).


CWI, P.O. Box 4079 			Arie van Deursen (arie@cwi.nl)
1009 AB Amsterdam
The Netherlands			   Ich weiss nicht was soll es bedeuten ...
Tel. 31 20 5924007

In article <3572@charon.cwi.nl>, arie@cwi.nl (Arie v. Deursen) writes:
> 
> An excellent _book_ on formal specifications is:
> @BOOK{GM86,
>   KEY           = "GM86",
>   EDITOR        = "N. Gehani and A.D. McGettrick",
>   TITLE         = "Software specification techniques",
>   PUBLISHER     = "Addison-wesley publishing company",
>   YEAR          = 1986
> }
> 
> The book brings together 21 important (and by now sometimes "classical")
> articles on (formal) specification. The articles are grouped in four sections,
> each of which considers a particular aspect of the subject.
> The book is from 1986, so _very_ recent articles are not covered.

This is a nice collection, but VERY out of date.  Although the publication date
is 1986, all the articles except one are about 10 years old or even older.
I don't know about other specification techniques, but algebraic specification
techniques (which I do know about) have advanced practically out of recognition
since then.

Don Sannella
University of Edinburgh

P.S. A fairly up-to-date survey (NOT a tutorial) of work on algebraic specification
with an extensive bibliography is the following.

M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas and D. Sannella (editors).
Algebraic System Specification and Development: A Survey and Annotated Bibliography.
Springer Lecture Notes in Computer Science (1991).

This is due to appear any day now.