timc@cs.man.ac.uk (Tim Clement) (08/21/90)
Are there any textbooks on algebraic approaches to formal specification? (Or, indeed, anyone teaching it at an undergraduate/Masters level?) Reply by mail and I'll summarize to the net if there's any interest. Thanks in advance for your help.
timc@cs.man.ac.uk (Tim Clement) (08/30/90)
I received 14 replies to my enquiry about textbooks in the area of algebraic specification. As promised at the time, I am summarizing them here. As this is a summary, I have taken the liberty of editing out some of the suggestions which seemed to be getting more peripheral to what I intended by the original posting. I also had some replies along the lines of "X teaches a course on this and you could ask him for his notes" which I am following up, but where I felt that it was unreasonable to give X what might be unwanted publicity. Three books were widely suggested. I have collected the comments on each of them together into a single list. [Ehrig and Mahr 85] Ehrig, H., and Mahr, B. Fundamentals of Alge- braic Specification 1: Equational and Initial Semantics, EATCS Mono- graphs on Theoretical Computer Science, Vol. 6. Springer-Verlag, Berlin, 1985. [Ehrig and Mahr 90] Ehrig, H., and Mahr, B. Fundamentals of Al- gebraic Specification 2: Module Specifications and Constraints, EATCS Monographs on Theoretical Computer Science, Vol. 21. Springer-Verlag, Berlin, 1990. From: jsf@uk.ac.man.cs: > Vol 1 is on the mathematical fundamentals. Volume 2 has just been > published and deals with (I think, though I haven't had a chance to > read it yet) modularity, refinement and the like. I wouldn't suggest > them as buys for taught courses, but they might be of use in > formulating course material. And they are "Important". > A lot of the concepts related to AS described in the books esp. > refinement and modularity are very much research material i.e. there > isn't a great concensus yet. From: sharif_el_kassas <elkassas@nl.tue.ele.eb>: > A [...] theoretical introduction to fundamental topics in AS. From: Vance Morrison <morrison@edu.uiuc.cs>: > [...] theoretical and harder to read [than Wirsing and Bergstra]. From: Y V Srinivas <srinivas@edu.uci.ics.madeleine>: > The monographs by Ehrig and Mahr are a textbook style introduction to > equational specifications, initial semantics, modules, and > specifications with constraints. From: Ping Lin <ping@edu.toronto.hub>: > [...] quite theoretically detailed. From: Frank Pohl <thomson@com.sri.unix>: > This would be recommended for a Masters level. Uses category theory > to a certain extent. From: Patrick Goldsack <pcg@com.hp.hpl.hplb>: > [Vol. 1] is a very clear and concise account (if you can put up > with the english and the type-face), ending with a couple > of chapters on the ACT 1 language (the basis of LOTOS data typing). [Bergstra, Heering & Klint 89] Bergstra, J.A., Heering, J., and Klint. P. (eds). Algebraic specification. ACM Press, New York 1989. 397 pp. ISBN 0-201-41635-2. ACM order # 704890. (ACM Press frontier series) From: sharif_el_kassas <elkassas@nl.tue.ele.eb>: > [...] a collection of papers covering different aspects of AS and > I think would be a nice complement to [Ehrig&Mahr]. From: "Pablo A. Straub" <straub@edu.umd.cs>: > [...] might be useful, but it is not a textbook. From: Vance Morrison <morrison@edu.uiuc.cs>: > [...] perhaps the best of the three [Ehrig&Mahr,Wirsing&Bergstra]to > start with, however, I would not call it a 'beginners' book either. From: Kevin Greene <greene@com.mcc> > The book claims to focus (I have not read it yet) on these three areas: > - the design of algebraic spec formalisms > - application of alg. spec techniques to the defn of prog langs > - the generation of exec. prototypes from alg. specs From: Y V Srinivas <srinivas@edu.uci.ics.madeleine> > The book by Bergstra et al. is less theoretical, with > the emphasis on using algebraic specification for describing the > semantics of programming languages From: Ping Lin <ping@edu.toronto.hub> > [...] a very readable introduction [Horebeek and Lewi 89] Horebeek, I. V., and Lewi, J. Algebraic Spec- ifications in Software Engineering: An Introduction. Springer-Verlag, Berlin, 1989. ISBN 3-540-51626-3, 0-387-51626-3. From: Eric Van Gestel <ericvg@uucp.kulcs>: > It is a didactical rewrite of the first author's PhD thesis and covers: > - the mathematical foundations (oriented towards a pragmatic audience); > - the design of a practical, constructive specification language; > - two medium-sized case studies showing how it can be used; > - a method for specifying exceptional cases (error handling) > [also published in Software - Practice and Experience, May 1988]; > - a development of abstract implementations. > > Our main incentive in writing the book (parts of which have been used since > 1984) was that we could not find any textbook suited for the curriculum > (both undergraduate and graduate levels) of 'software engineers' with a > proper balance between theoretical foundations and practical > applicability, so we set out to bridge the gap. From: sharif_el_kassas <elkassas@nl.tue.ele.eb>: > didn't read it ;-> yet but seems to have lots of examples ... From: Y V Srinivas <srinivas@edu.uci.ics.madeleine>: > [...] is an introduction to algebraic specification with an emphasis > on applying it in software engineering; a variety of concepts are > introduced at an intuitive level, and some non-trivial examples are > included. From: Ping Lin <ping@edu.toronto.hub> > [...] closer to being a textbook [...] The remaining books were suggested by a single person (many of whom have already appeared above), and I have left their comments (almost) unedited. From: Vance Morrison <morrison@edu.uiuc.cs> > Algebraic Methods: Theory Tools and Applications > Lecture Notes in Computer Science 394 > M. Wirsing, J.A. Bergstra (eds) > Springer-Verlag 1989 > [...] a collection of papers, nevertheless, the papers are pretty readable, > and in general useful. From: David Murphy <dvjm@uk.ac.glasgow.cs>: > For more concurrency-oriented topics, > Hennessy, the Algebraic Theory of Processes (MIT) is more > algebraic than either of the standard books by Milner or Hoare. > I'm not sure I'd want to teach all of an undergraduate course > from it, but it does have its moments. From: eerke@nl.kun.cs: > Below is an excerpt from the bibtex database I maintain on software > engineering and program development. I can't tell you more about many of > the books (since I didn't read most of them) but this may be of some > use: > @BOOK{ > Ehr??, > Author= {Ehrich, H.-D. and Lipeck, U.W. and Gogolla, M.}, > Title= {Algebraic Specifications}} > @BOOK{ > Par90a, > Author= {Partsch, H.}, > Title= {Specification and Transformation of Programs - a Formal > Approach to Software Development}, > Address= {Berlin}, > Publisher= {Springer-Verlag}, > Year= 1990} From: Y V Srinivas <srinivas@edu.uci.ics.madeleine>: > Here are some references extracted from my survey, "Algebraic > Specification: Syntax, Semantics, Structure", Technical Report 90-15, > Dept. of ICS, University of California, Irvine, June 1990, 132 pp. > =========================================================== > BOOKS ON ALGEBRAIC SPECIFICATION > > The monograph by Reichel describes equational specifications > with partial operations and initial restrictions [Reichel 87]. The > book by Turski and Maibaum introduces algebraic specification in the > context of software development; the book is well written, with > balanced proportions of formal and informal material [Turski and > Maibaum 87]. The monograph by Padawitz discusses Horn clause > specifications, with an emphasis on rewriting techniques [Padawitz 88]. > The chapter on abstract data types in [Bauer and Wossner 82] is a good > introduction to the algebraic approach; the density of good concepts > in this book demands careful reading. > > REFERENCES > > [Bauer and Wossner 82] Bauer, F. L., and Wossner, H. Algorithmic > Language and Program Development. Springer-Verlag, Berlin, 1982. > > [Padawitz 88] Padawitz, P. Computing in Horn Clause Theories, EATCS > Monographs on Theoretical Computer Science, Vol. 16. Springer-Verlag, > Berlin, 1988. > > [Reichel 87] Reichel, H. Initial Computability, Algebraic Specifications, > and Partial Algebras. Oxford University Press, 1987. > > [Turski and Maibaum 87] Turski, W. M., and Maibaum, T. S. E. The > Specification of Computer Programs. Addison-Wesley, 1987. From: "Peter D. Mosses" <pdmosses@dk.aau.daimi> > I recently gave an M.Sc. level one-semester course on algebraic > specification here at Aarhus. As most of the students hadn't seen any > category theory before, we started by skimming Chapter 2 of: > > Benjamin Pierce: > "A Taste of Category Theory for Computer Scientists" > Tech. Report CMU-CS-88-203, Carnegie-Mellon. > > (I believe a new version is available now.) Highly recommended! > > Then we went through all but the computability results of > > Martin Wirsing: > "Algebraic Specification" > Tech. Report MIP-8914, Passau > (to appear as a chapter of > "The Handbook of Theoretical Computer Science", Volume B, > Elsevier/MIT Press, October? 1990). > > It wasn't intended for use as a textbook! One has to invent one's own > exercises, and some of the material is rather tough going for the > students. But it has the great advantage (over the other texts I saw) > of being elegant, up-to-date, and comprehensive. It presents the > framework of loose total algebra specifications, and defines a kernel > module specification language, Sannella-Tarlecki-Wirsing style. It > also includes summaries of other major approaches. > > The rest of the course consisted of practicals: each group of students > had to read about a particular system (OBJ3, RAP, ASSPEGIQUE, LP) and > write an assessment of the system, explaining the theoretical base of > the system in relation to Wirsing's framework and reporting how well > the system (as implemented) supported the development of a modest > specification, taken from: > > John Guttag, Jim Horning: > "Formal Specification as a Design Tool" > Proc. POPL'80. > > - also highly recommended! I was also told that a similar survey had been done recently in comp.theory. I am attempting to trace this. Many thanks to all my respondents for their answers. Tim