🚀 go-pugleaf

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