Chalmers & GU, Monday 02/06 to Friday 06/06, 2003.

June 06: for the 5th lecture, you may print A Gentle Introduction to CASL (slide set, handout)

June 05: Fourth slide set (handouts) added.

June 04: Third slide set (handouts) added.

June 03: Second slide set (handouts) added.

June 02: First slide set (handouts) added.

May 28: The time of the morning lectures is made more specific: 10.15-12.00.

May 26: This is the first version of the course page. Please visit the page again and check for changes, which will be announced in this section.

Data types are omnipresent in Computer Science. In the context of
programming, they appear (at least) on two levels. One the one hand,
programs *use* data types provided by the according language. (Some
languages offer the user to define further data types which can be
used in the program.) On the other hand, in the opposite direction,
certain programs may *realize* a data type. In that context, the data
type, or it's description, serves as a *specification* of the program.
In the term "Abstract Data Type", "abstract" refers to different
things: First, one wants to stress that we are concerned with the data
types themselves and not with their implementation. Second, we also
consider data types that are intentionally incompletely defined, with
irrelevant details left pending. Related to this is the view that an
"abstract" data type represents a whole class of data types with
"similar" properties.

One way to describe an abstract data type is to state its properties as
axioms, which relate the operations of the data type to each other.
This `axiomatic' approach to abstract data types, and the according
research field, is also called `*Algebraic Specification*'. Even if it
is strongly related to logic, it is rather rooted in the field of
universal algebra. One difference to the mainstream of the logical
tradition is the presence of semantical assumptions, which allow to
naturally describe data types that are otherwise not expressible by,
for example, first-order logic. At the same time, these assumptions make
the use of higher-order logic in the axioms superfluous. As a result,
algebraic specification languages work with a very simple syntax
of axioms, while providing the expressiveness needed for many computer
science applications. Accordingly, examples of algebraic
specifications (like the specification of a stack) are often shown
even to beginner students, which without any theoretical background can
grasp the basic idea.

- theoretical foundations of algebraic specification
- different algebraic specification styles
- loose
- initial
- constructive

- connections to
- logic
- rewriting
- program verification
- model generation (if there is time left)

- the specification language
CASL

(the recent quasi standard provided by CoFI)

The content of the course has a theoretical nature. The course however aims at
*all* Ph.D. students at the department, no matter which field they are
working in. Particularly, nobody is assumed to even have heard
of algebraic specification before. Many examples will anyhow turn out
to be pretty much `folklore', but not to the depth we will discuss
them.

The course will take place every day (Mon to Fri) at 10.15-12.00 and 16.15-18.00. The location is MD10, with the exception of Tuesday morning (MD9).

Morning sessions are for lectures. At the end of the lecture, exercises are given, and the students will work on them during the beginning of the afternoon. In the afternoon session, we discuss the solutions.

- Course Slides (the slide sets do not coincide with the
partitioning into lectures):

Slide Set 1, Slide Set 2, Slide Set 3, Slide Set 4, (handout), for the 5th lecture, you may print A Gentle Introduction to CASL (slide set, handout)

- J. Loeckx, H.-D. Ehrich, M. Wolf

*Specification of Abstract Data Types*

Wiley and Teubner 1996 - J. Loeckx, H.-D. Ehrich, M. Wolf

*Algebraic specification of abstract data types*

in:

S. Abramski, D.M. Gabbay, T.S.E. Maibaum (Eds.)

*Handbook of Logic in Computer Science*

Oxford University Press 2000 - M. Wirsing

*Algebraic Specification*

in:

J. v. Leeuwen (Ed.)

*Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics*

Elsevier and MIT Press 1990