Topic outline
 
Formal Specification of Abstract Datatypes
(326.038, WS 2005/06)
Time:
Thursday 17:15-18:45.
Place: T 041.
Start: October 6.

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).


To take part in the course, you have to enrol in the KUSSS system. Please also register for this Moodle course (link "Login" on the upper right corner), then you will automatically receive per email all messages posted in the "News" forum below.

Forum News forum
 
1
Presentations
Literature

Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf: Specification of Abstract Datatypes, John Wiley & Teubner, Chichester, 1996. Amazon Page.

Restricted Material

The content of this section is protected; the corresponding password is handed out in class. It is strongly forbidden to forward this password to anyone not participating in the course.

2
CafeOBJ

The CafeOBJ system is freely available for Linux and Windows from the CafeOBJ home page.

Local copies:
Resource How to Use CafeOBJ at RISC

3
Exercises
Resource Exercises

4
Course Evaluation

At the end of the semester, please fill the evaluation sheet and send it per university mail to the "Institut für Symbolisches Rechnen (Sekretariat)".

Resource Course Evaluation