Foundations of Algebraic Specification and Formal Software Development

by Donald Sannella and Andrzej Tarlecki.
EATCS Monographs in Theoretical Computer Science.
Springer, 2012. ISBN 978-3-642-17335-6.

Order from Amazon (reviews) or Springer.


0. Introduction
1. Universal algebra
2. Simple equational specifications
3. Category theory
4. Working within an arbitrary institution
5. Structured specifications
6. Parameterisation
7. Formal program development
8. Behavioural specifications
9. Proofs for specifications
10. Working with multiple logical systems
Index of categories and functors
Index of institutions
Index of notation
Index of concepts

The complete table of contents is here and the concept index is here.


p124, Definition 3.3.1 (Factorisation system): K at the end of the third bullet point should be M.
p238, Enrichment, notational variants: S and Π should be S' and Π'
p420-421, Exercise 9.2.10: If a finitely exact institution satisfies the Craig-Robinson interpolation property and comes equipped with a sound and complete entailment system, then the entailment defined by the proof rules for consequences of specifications built from flat specifications using union, translation and hiding with the infinitary version of (*) is complete, see D. Sannella and A. Tarlecki. Property-oriented semantics of structured specifications. Mathematical Structures in Computer Science 24(2), e240205 (2014). One does not have to assume that semantic consequence is reflected by translation of sentences along signature morphisms, and the counterexample required in the exercise cannot be provided.
p536, Bibliography, [CDE+02]: Clavela should be Clavel

Please send bug reports to the authors.

Answers to exercises

Answers to exercises contributed by readers are welcome and will be published here once they have been checked for correctness. Any reader submitting an answer will be rewarded with a hint for an exercise of his/her choice from the same chapter.

Don Sannella and Andrzej Tarlecki.
Last modified: Sun Sep 16 23:23:13 BST 2012