Spezifikationstechniken

- Allgemeines & Ankündigungen -

DI 13 - 15 h

DI 15-16

Dienstag, 19.12.2006: Beginn 13:00 (s.t.)

Einführung: Folien

1. Grundlagen
1.1 Signaturen als Spezifikationsbestandteil: Folien
1.2 Formeln und Erzeugungsforderungen: Folien

2. Initiale Spezifikation abstrakter Datentypen:
Folien - 1 (PS) Folien - 2 (PS) (PDF)

3. Lose Spezifikation abstrakter Datentypen: Folien (PS) (PDF)

4. Spezifikationssammlungen und -operationen:
Folien - 1 (PS) (PDF) Folien - 2 (PS) (PDF)

5. Verfeinerung, Erweiterung und abstrakte Implementierung:
Folien - 1 (PS) (PDF) Folien - 2 (PS) (PDF)

6. Exkurs über partielle Funktionen, Fehlerwerte und Untersorten:
Folien (PS) (PDF)

7. Konstruktive Spezifikationen und Termersetzungssysteme:
Folien (PS) (PDF)

8. Zustandsorientierte Spezifikation:
Folien (PS) (PDF)

9. Algebraische Spezifikation mit CASL:
Folien (PS) (PDF)

10. Modellbasierte Spezifikation mit Z:
Folien (PS) (PDF)

11. Temporale Spezifikation reaktiver und nebenläufiger Systeme:
Folien (PS) (PDF)

Ziel der Vorlesung ist es, Grundkenntnisse über die wichtigsten Methoden der formalen Spezifikation zu vermitteln.

Inhalte sind insbesondere:

Spezifikation abstrakter Datentypen: initiale und lose Spezifikation

Spezifikationssammlungen und -operationen

Verfeinerung, Erweiterung und abstrakte Implementierung

Konstruktive Spezifikationen

algebraische Spezifikation mit CASL

modellbasierte Spezifikation mit Z

temporale Spezifikation nebenläufiger Systeme

In der Druckversion der Folien (nicht in der Originalpräsentation) zu Abschnitt 4, Teil2, (ST06F4-2) fehlt auf Folie "p.12" ein Unterpunkt, nämlich:

"- Die Argumentspezifikation darf kein Symbol, das in < SpezRumpf > neu deklariert wurde, enthalten."