Modulcode: | Inf-AlgSpec |
Englische Bezeichnung: | Algebraic Specification |
Modulverantwortliche(r): | Prof. Dr. Dirk Nowotka |
Turnus: | unregelmäßig (SS14 SS15 SS16) |
Präsenzzeiten: | 2V 2Ü |
ECTS: | 6 |
Workload: | 30 Std. Vorlesung, 30 Std. Präsenzübung, 120 Std. Selbststudiu |
Dauer: | ein Semester |
Modulkategorien: | TI (MSc Inf (15)) WI (MSc Inf (15)) WI (MSc WInf (15)) WI (MEd Inf) WPI (MEd Inf) IG (MSc Inf) IS (MSc Inf) MV (MSc Inf) |
Lehrsprache: | Englisch |
Voraussetzungen: | Inf-TGI |
This course is an introduction into the theory of algebraic specification, a software engineering technique used to describe mathematically the properties and behaviour of informatic systems and then to reason about them. Our intention is to develop the mathematical framework of this technique and then to illustrate its usage to specify different, from simpler to more complex, data types, to specify algorithms, and to check automatically properties of these data types and algorithms. Alongside the mathematical foundations of algebraic specification we also present an algebraic specification programming language, CafeOBJ.
We expect that the participants to this course will gain a good understanding of the mathematical foundations of algebraic specification and will able to use this technique to specify on their own different data types or algorithms. Also, they are supposed to aquire a good command of the CafeOBJ programming language, and use it to specify data types and algorithms, and automatically prove properties of these objects.
The main topics our course will cover are: Basic data type specification, Structured specifications, Algorithm Specification and Verification, Algorithm verification, Abstract Machines, Basic behavioural specification, Behavioural proofs, Object composition. The presentation of each topic from the above consists in presenting its mathematical foundations, describing the way it is actually used, and showing examples of its usage.
basic knowledge in theoretical computer science and mathematical logic
oral exam after the course
lecture with beamer and black board presentation; exercises
http://www.ldl.jaist.ac.jp/cafeobj/