*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.

## Contents

- Preface
- 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
- Bibliography
- 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.

## Errata

- 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