Formal Specification of Abstract Datatypes (SS 2020)
Abschnittsübersicht
-
326.076/326.0VR, Friday 8:30-10:00, HS 13, Start: March 6, 2020
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 and logic 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 sketch the object-oriented specification languages Larch/C++ and JML which are based on similar principles and finally introduce the Common Algebraic Specification Language CASL.
Presentations of various case studies are interspersed. Course grades will be based on exercises which are both theoretical (paper and pencil) and practical (CafeOBJ).
To take part in the course, you have to enrol in the KUSSS system. Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the News forum.
-
The lecture will be based on a not yet published manuscript "Thinking Programs" that covers in Chapter 6 the topic of "Abstract Data Types"; in the course we will walk through parts of this chapter.
- Chapter 6: Abstract Datatypes (teaser excerpt only)
- Thinking Programs (draft manuscript, password will be handed out in class)
Variously we will also use slides and other material from previous instances of this course (not aligned with above chapter):
- Introduction (4 on 1).
- Abstract Datatypes (4 on 1).
- CafeOBJ (4 on 1).
- Logic (4 on 1).
- Specifications: Formal and Informal - A Case Study (restricted)
- Specifications: Formal and Informal - A Case Study (restricted)
- Term Algebras (4 on 1).
- Initial Specifications (4 on 1).
- Executing Specifications (4 on 1).
- Specifying in the Large (4 on 1).
- Case Study - A Multiple Window Environment (restricted)
- A Case Study - A Lexical Analyzer (restricted)
- A Gentle Introduction to CASL (original site).
Restricted Area (password handed out in class)
Literature
Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf: Specification of Abstract Datatypes, John Wiley & Teubner, Chichester, 1996. Amazon.at Page.Donald Sannella, Andrzej Tarlecki: Foundations of Algebraic Specification and Formal Software Development, Springer, Berlin, 2012. Amazon.at Page.
Wolfgang Schreiner: Thinking Programs (Chapter 6, restricted). - Chapter 6: Abstract Datatypes (teaser excerpt only)
-
The CafeOBJ system is freely available for Linux, MacOS, and Windows from the CafeOBJ home page.
If necessary, you may also use the CafeOBJ installation in the RISC environment (see the Course Software at RISC).
-
Grades will be issued on the basis of five exercises that will be issued during the semester (the best four ones will be used for grading).