The goal of this course is to teach students of computer science and mathematics methods for the formal specification of abstract data types and their application in practical software engineering examples. No prerequisites apart from basic set theory are required.

We concentrate on the approach of algebraic/axiomatic program specification where concepts from universal algebra are used to formalize the semantics of specifications. For rapid prototyping, we use the software system CafeOBJ in which specifications can be directly executed. We also introduce the Common Algebraic Specification Language CASL and sketch the object-oriented specification languages Larch/C++ and JML which are based on similar principles.

Presentations of various case studies are interspersed; exercises are both theoretical (paper and pencil) and practical (CafeOBJ).