Formal Specification of Abstract Data Types
326.511, WS 2002/2003
Start: October 10, 2002
December 11: 10:15-11:45, T212
The class on December 12 is cancelled.
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 examples. No prerequisites apart from basic set
theory are required.
We concentrate on the approach of algebraic program specification where
concepts from universal algebra (many-sorted algebras) are used to formalize
the semantics of specifications. For rapid prototyping, we use the
in public domain for any Unix or Linux computer) in which specifications can
be directly executed.
Students are expected to elaborate exercises and to present them in class.
- Many-sorted algebras
- Algebra logics
- Specifications in the small
- Specification languages
- Modularization and parameterization
- Case studies
- Jacques Loeckx and Hans-Dieter Ehrich and Markus Wolf
Specification of Abstract Data Types, Wiley & Teubner,
Chichester, UK, 1996.
- Ivo van Horebeek and Johan Lewi
Algebraic Specifications in Software Engineering, Springer,
Berlin, Germany, 1989.
- Narain Gehani and Andrew McGettrick (eds)
Software Specification Techniques, Addison Wesley, Wokingham, UK, 1986.
- Ataru T. Nakagawa and Toshimi Sawada and Kokichi Futatsugi
CafeOBJ User's Manual -- ver.1.4,
CafeOBJ Homepage (Japan).
- Joseph A. Goguen et al.
Introducing OBJ, Technical Report,
Programming Research Group, Oxford University, UK, October 1993.
Maintainer: Wolfgang Schreiner
Last Modification: December 10, 2002