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

Kurzfassung:

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.

Lernziele:

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.

Lehrinhalte:

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.

Weitere Voraussetzungen:

basic knowledge in theoretical computer science and mathematical logic

Prüfungsleistung:

oral exam after the course

Lehr- und Lernmethoden:

lecture with beamer and black board presentation; exercises

Verwendbarkeit:

Literatur:

• CafeOBJ official web-page: http://www.ldl.jaist.ac.jp/cafeobj/
• Razvan Diaconescu and Kokichi Futatsugi: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification; Amast Series in Computing, Vol.6, World Scientific, 1998.
• Dershowitz, N. and Jouannaud, J.-P.: Rewrite Systems, Handbook of Theoretical Computer Science, Vol.B: Formal Models and Semantics, The MIT Press/Elsevier Science Publishers, 1990, pp.245-320.
• Ehrig, H. and Mahr, B.: Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics, Springer-Verlag, 1985.
• Klop, J.W., Term Rewriting Systems: A Tutorial, EATCS Bulletin, No.32, EATCS, 1987, pp.143-182.

Verweise:

Kommentar: