Formal Specification of Abstract Datatypes (SS 2022)
Section outline
-
326.076/326.0VR, Friday 8:30-10:00, Room: HS 13, Start: March 11, 2022
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 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 (user manual) in which specifications can be directly executed and also sketch the Common Algebraic Specification Language CASL (a gentle introduction).
Course grades will be based on homework assignments which are both theoretical (paper and pencil) and practical (CafeOBJ).
To participate in the course, you have to register in the KUSSS System. Since the assignments will be uploaded in Moodle, you also have to create an account in the RISC Moodle (press the button "Create new account") and self-enrol in the course (press the button "Enrol me"); then you also receive all messages posted in the course forums per email.
-
As an extra service, it is intended to live-stream and record the lectures via the following Zoom meeting:
https://jku.zoom.us/j/93821818291?pwd=dVRFR3NEcFd5OWxhWnp4ZzVnMVU2UT09
Meeting-ID: 938 2181 8291 Password: adtHowever, no guarantee is given with respect to completeness and quality of the stream/recordings. The basic course format is on-site, not hybrid.
-
The lecture will be based on Chapter 6 "Abstract Datatypes" of the book "Thinking Programs"; in the course we will walk through most parts of this chapter (the book can be freely downloaded from the JKU campus network).
Additional Material
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, Springer, Cham, Switzerland, 2021. Amazon.at Page. -
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 assignments that will be issued during the semester (the best four ones will be used for grading).
-