srinivas@ics.uci.edu (Yellamraju Srinivas) (07/13/89)
In article <5545@tekgvs.LABS.TEK.COM> gregho@tekgvs.LABS.TEK.COM (Greg Hoffman) writes: > >I'd like to locate a good survey book or article on algebraic specification. >I've run across a reference to Ehrig and Mahr's book, "Fundamentals of >Algebraic Specification". I'd be interested in any opinions on this text or >any pointers to other references. There are a variety of styles of algebraic specification, and as far as I know, there is no comprehensive survey available on this subject. I think the best place to start is Goguen's paper on parameterized programming (reference appears below). ***** BOOKS ***** H. Ehrig and B. Mahr: Fundamentals of Algebraic Specification 1: Equational and Initial Semantics. Springer-Verlag, 1985. An excellent introduction to the *theory* of algebraic specification. However, it only treats specifications which have total functions, equations as axioms, and initial semantics. The first three chapters, and the description of the language ACT ONE in the appendix (chapter 9) are at an introductory level. Later on, they use some heavy mathematics, especially category theory. Volume 2 of this book should be available soon. J. A. Bergstra, J. Heering, P. Klint (eds.): Algebraic Specification. ACM Press and Addison-Wesley, 1989. This book is a collection of papers which use the algebraic specification language ASF to define the semantics of several toy programming languages. As opposed to the book of Ehrig and Mahr, this is much lighter reading. The first chapter is an introduction to the ASF language. The book contains lots and lots of algebraic specification examples. W. M. Turski and T. S. E. Maibaum: The Specification of Computer Programs. Addison-Wesley, 1987. This is not a book on algebraic specifications per se, but a book on a formal approach to software construction. What they call "linguistic systems" are closely related to algebraic specifications. They use sentences in first-order logic as the axioms in a specification. The semantics is loose, i.e, any model is acceptable. And specifications can be incomplete. They view the software construction process as the passage from a specification to a program via a sequence of linguistic systems. Any two consecutive linguistic systems are bridged by a so-called "generic design step", the primary purpose of which is to introduce design detail. The whole process is much like stepwise refinement, but in a much more formal setting. The book is well written and good not only for learning about algebraic specifications, but also to learn about how they can be *actually* used in software construction. The Munich Project CIP. Volume I: The wide spectrum language CIP-L. Lecture Notes in Computer Science, vol. 183, Springer-Verlag, 1985. The Munich Project CIP. Volume II: The program transformation system CIP-S. Lecture Notes in Computer Science, vol. 292, Springer-Verlag, 1987. The CIP project (Computer aided Intuition guided Programming) was started at TU Munich about 15 years ago, with the aim of building a system for the transformational construction of software using a wide-spectrum specification language which accommodates everything from specification to program. Volume I is a description of the wide-spectrum language. One part of the language consists of algebraic specifications with first-order logic axioms. You need some patience to wade through the details of the language. CIP-L examples can be also be found in the following paper: Bauer et al: Programming in a wide spectrum language: A collection of examples. Science of Computer Programming, vol. 1, pp. 73-114, 1981. Volume II contains a formal specification of the CIP transformation system (the intent was to bootstrap the system using a prototype). This is the largest algebraic specification which I have seen in print, and considering its size (120 pages) it is eminently readable. ****** PAPERS ****** Joseph A Goguen and Timothy Winkler: Introducing OBJ3. Tech. Rep. SRI-CSL-88-9, SRI International, Menlo Park, CA, August 1988. OBJ3 is a wide-spectrum functional programming language based on order-sorted equational logic. (Don't be fooled by this blurb: it is much more like algebraic specification than a conventional functional programming language). An implementation is available from SRI International. OBJ3 is perhaps the best algebraic specification language that is currently available. Both its denotational and operational semantics have been extensively studied. Joseph A Goguen: Principles of Parameterized Programming. In: Software Reusability, ed. Biggerstaff and Perlis, ACM Press, New York, pp. 159-225, 1989. OBJ3 supports parameterized programming, a powerful technique for building software in a modular way. The philosophy of parameterized programming, and the use of OBJ3 to realize this philosophy is described in this excellent paper. ******************************* If you are more theoretically inclined, here is a sampler: J. A. Goguen, J. W. Thatcher and E. G. Wagner: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology, vol.IV, ed. Raymond Yeh, Prentice-Hall, pp. 80-149, 1978. A seminal paper in this field, convincingly arguing that the semantics of an algebraic specification should be the initial algebra. Egidio Astesiano and Martin Wirsing: An introduction to ASL. In: IFIP TC2/WG2.1 Working Conference of Program Specification and Transformation, ed. Meertens, North-Holland, pp. 343-365, 1987. ASL is a sort of meta-language which can accommodate all other algebraic specification languages. It is based on the realization that the fundamental ingredients in an algebraic specification language are operations for "putting things together". J. V. Guttag and J. J. Horning: The algebraic specification of abstract data types. Acta Informatica, vol. 10, pp. 27-52, 1978. Guttag's thesis was one of the earliest contributions to this field. This paper contains a slightly modifed version of those ideas. More recent work by Guttag is on LARCH. Martin Wirsing, Peter Pepper, Helmut Partsch, Walter Dosch and Manfred Broy: On hierarchies of abstract data types. Acta Informatica, vol. 20, pp. 1-33, 1983. An introduction to the Munich school's ideas on algebraic specification. The distinguishing feature is that they allow partial operations, use quite general axioms, and adopt loose semantics (as opposed to initial semantics). ******************************* Yellamraju V. Srinivas Dept. of ICS, University of California, Irvine, CA 92717 -- Y V Srinivas
nagle@well.UUCP (John Nagle) (07/14/89)
Parnas' papers from the 1970s are relevant, and amusing at times. Parnas goes down in programming language history for claiming that variable names should be meaningless, so that readers of the specification are forced to follow the logic. John Nagle