department
wg bkb
Algebraic Specification
A course by Lutz Schröder at the Universität Bremen 2004/2005.
Reasoning about the correctness of programs is made possible only by having a way to express their intended behavour. This is the object of algebraic specification -- programs are regarded as algebras consisting of datatypes and operations, and the intended behaviour of a program is specified by means of formulas (say, equations) concerning these operations. The course provides an introduction to algebraic specification using the specification language CASL; it will partly be based on the script by Hans-Jörg Kreowski. A standard textbook on algebraic specification isJacques Loeckx, Hans-Dieter Ehrich, Markus Wolf: Specification of Abstract Data Types, Wiley/Teubner, 1996.
Teaching Material
- Slides etc. for the first lecture
- Slides: CASL examples
- Slides on signatures
- Slides on terms
- Problem Sheet 1
- In preparation for the first problem sheet:
- An introduction to parsec
- Index of the Haskell prelude (refresh your knowledge of list functions)
- Index of the ghc libraries (List/Char functions, parsec)
- Slides on substitution
- Slides on equational deduction
- Slides on rule induction and the substitution rule
- Problem Sheet 2
- Slides on algebras
- Slides on the correctness theorem
- Slides on term algebras
- Slides on properties of term algebras
- Problem Sheet 3
- Slides on existence and uniqueness of initial algebras
- Slides on Homomorphisms
- Slides on Set-theoretic Quotients
Author: Dr. Lutz Schröder
| Last updated: January 25, 2005 |  |