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