The aim is to present one approach to formal specification, verification and formal development in some detail. Students will learn how to write specifications, what they mean, how to reason about them and how to use them in developing modular software systems. The emphasis will be split evenly between practice ("how to write and use specifications") and theoretical foundations ("what they mean" etc.).For undergraduates, this would build on the basic introduction to formal specifications in the CS3 module Functional Programming and Specifications. The FPS module is strongly recommended before this one but does not need to be a formal prerequisite. For MSc and PhD students, a prior introduction to formal methods would be an advantage.
The theory part of the course can be adjusted according to the inclinations of the participants. A mimimum would be the first two items, which corresponds to the classical material on algebraic specification. LFCS PhD students attend a course on category theory that goes far beyond item 4, and these students may skip that part of this course.
1. Motivation. Modelling systems as algebras, describing functional behaviour, formal software development.Strand A: Theory
2. Universal algebra: signatures, algebras, homomorphisms, congruences, term algebras, term evaluation, signature morphisms, reducts.
3. Simple equational specifications: satisfaction and the Satisfaction Lemma, flat specifications, Birkhoff Variety Theorem, theories, equational calculus, initial models, structural induction, term rewriting.
4. Basic category theory: categories, duality, epis, monos, isos, limits and colimits, functors and natural transformations, freeness.
5. Working within an arbitrary logical system: institutions, flat specifications in an arbitrary institution, institutions with extra structure.
6. Structured specifications: specification-building operations and their semantics, how to roll your own, specification languages, the category of specifications, algebraic laws for structured specifications
7. Further topics: parameterised specifications, parameterised programs, and specifications of parameterised programs; extending to higher-order; formal program development, stepwise development, modular decomposition; behavioural equivalence, behavioural abstraction, modular development and stability; proving theorems about modular specifications; the category of institutions, heterogeneous specifications.
Strand B: Practice
8. The Common Algebraic Specification Language (CASL). Basic specifications, subsorts, structured specifications, generic specifications, views, architectural specifications. Methodological issues.
9. Using the CASL tool set.
The course will be assessed via at least two written exercises -- one on the practical strand, one on the theory strand -- and a project on specification and formal development of a small modular system.
D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229-269 (1997).Selected parts of the draft of the book: D. Sannella and A. Tarlecki. Foundations of Algebraic Specification and Formal Program Development.
M. Bidoit and P. Mosses. CASL user manual, 2002.
Other papers from the research literature.