straub@jogger.cs.umd.edu (Pablo A. Straub) (05/11/91)
Which do you think is THE tutorial paper on formal specification of requirements? I want to give one paper or book chapter as required reading for undergraduate students in a Software Engineering course. Thanks for your responses Pablo Straub
straub@jogger.cs.umd.edu (Pablo A. Straub) (05/21/91)
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. ------------------------------------------------------------------------
jack@dcs.glasgow.ac.uk (Jack Campin) (05/21/91)
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
haim@taichi.uucp (24122-Haim Kilov(L028)m000) (05/21/91)
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
pyoung@axion.bt.co.uk (Pete Young) (05/22/91)
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
arie@cwi.nl (Arie v. Deursen) (05/22/91)
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 5924007dts@cs.ed.ac.uk (Don Sannella) (05/23/91)
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.