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