Lecture on Algebraic Specification

Algebraic Specification

a course by Till Mossakowski and Markus Roggenbach at the Universität Bremen , 1999, VAK 3-631.

Introduction:

The course provides a thorough introduction to both theory and practice of algebraic specification.

The aim of algebraic specification is the design of reliable software. It allows for correctness by stepwise refinement, starting with an abstract specification closely related to the informal requirements and leading to an executable specification near to implemented code. Thus, seen as a formal method for software design, algebraic specification belongs to the area of software engeneering. However, it is usually classified as a discipline of theoretical computer science, since its foundations stem from logic.

The course starts with a short introduction to sigma-algebras, discusses the use of different logics (equational logic, conditional equational logic, first-order predicate logic) for algebraic specification, and presents selected topics of specification-in-the-small as well as specification-in-the-large. The concepts introduced are motivated by practical examples. Easy exercises for ``learning by doing'' provide a deeper understanding of the material presented.

The language used for the examples and small case studies is CASL (Common Algebraic Specification Language), an algebraic specification language (the design of this language has been recently finished, for current informations see the homepage of "The Common Framework Initiative (CoFI)" and our local CoFI Bremen homepage), which includes all concepts treated in the lectures. The choice of CASL closely relates this course to active and ongoing research, in particular it gives the opportunity to play around with several CASL tools.

Outline of the Course:

Basic Notions: Signatures, algebras, and terms.
Logic: A tool to characterize algebras.
Extension I: (Freely) generated algebras and (free) constructors.
Extension II: Combining specifications.

Lecture Times:

Tuesday, MZH 5290, 3-5 pm
Thursday, MZH 5300, 10-12 am

Beginning: Tuesday, October 26th 1999.

Examinations:

To obtain a certificate it it necessary to

solve four coursework exercises,
present the solution of an exercise in the lectures, and
succeed to an oral examination in the week 14.2.-18.2.00.

References:

There are many textbooks on Algebraic Specification. Among others, we use for our course

Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf: Specification of Abstract Data Types. Wiley, Teubner 1996.
J.A. Bergstra, J. Heering, R. Klint: Algebraic Specification. ACM Press and Addison-Wesley 1989.

For general information on the language CASL (Common Algebraic Specification Language), see the homepage of "The Common Framework Initiative (CoFI)". Documents of special interest for the course are the

CASL Summary (This document gives a detailed summary of the syntax and intended semantics of CASL.)
Basic Datatypes in CASL (This is the standard library of CASL specifications, which also illustrates how to write and structure specifications in CASL. As these specifications make use of partial functions and subsorting, which are not treated in the course, this document is of limited interest for the lectures. )
CASL Semantics (In this document the intended semantics of the CASL Summary is formulated in a strict mathematical way. We give the reference only for the interested students. The treatment of the semantics of an algebraic specification language in this document is out of the scope of our course.)

CASL-Tools:

Author: Dr. Markus Roggenbach

AG BKB

Last updated: August 5, 2002