Formal Specification of Abstract Data Types

326.511, WS 1998/99, HA 105, 16:30-18:00 (Start: October 8)
http://www.risc.uni-linz.ac.at/courses/ws98/specadt
Wolfgang Schreiner <Wolfgang.Schreiner@risc.uni-linz.ac.at>

Please note that the course takes place in Hagenberg!

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 software system CafeOBJ (available in public domain for any Unix or Linux computer) in which specifications can be directly executed. We put the presented techniques into context by contrasting them with the alternative approach of state-oriented specifications in the language Z.

Students are expected to elaborate exercises and to present them in class.

Contents

• Many-sorted algebras
• Algebra logics
• Specifications in the small
• Specification languages
• Modularization and parameterization
• Case studies
• State-oriented specifications

Literature

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.3,
CafeOBJ User's Manual -- ver.1.4.
CafeOBJ Homepage (Romania), CafeOBJ Homepage (Japan).

Joseph A. Goguen et al.

Introducing OBJ, Technical Report, Programming Research Group, Oxford University, UK, October 1993.

Ben Potter and Jane Sinclair and David Till

An Introduction to Formal Specification and Z, Second Edition, Prentice Hall International Series in Computer Science, London, UK, 1996.

Exercises

Exercises 1-3

1. Loose specifications
   1. Specify the integers by a loose specification with constructors.
   2. Specify the integers by a loose specification with free constructors.
   3. Show that both specifications define the same abstract datatype.
2. Initial specifications
   1. Specify the integers by an initial specification.
   2. Show that this specification is adequate by using the proof technique of characteristic term algebras.
3. Constructive specifications
   1. Specify the integers by a constructive specification.
   2. Implement this specification in CafeOBJ.
   3. Use this implementation to show the distributive law by induction.

Project

Create a specification of the expanded vocabulary system described in the accompanying document consisting of

1. a formal loose specification (with [free] constructors) presented in a nice way with ample natural-language explanations.
2. a rapid prototype implementation in CafeObj with some sample runs that demonstrate the essential aspects.

Solution 1, Solution 2