Vorlesung "Einführung in die formale Spezifikation von Software"
INBB03 - 4.1.10 V2 BSc Inf CV IM (Wahlpflicht) - KLIPS
INBB03 - 4.1.11 U2 BSc Inf CV IM (Wahlpflicht) - KLIPS
Vorlesung im Wintersemester 2008/2009
Prof. Dr.
Bernhard Beckert
Vladimir Klebanov
Die Webseite befindet sich im Aufbau - demnächst mehr
Aktuelles
31.01.09: Folien zur Spezifikationssprache Z.
31.01.09: Weiteres Beispiel zur Algebraischen Spezifikation.
16.12.08: Materialien zur Algebraischen Spezifikation.
29.11.08: Die Folien zur Vorlesung und zur Übung dieser Woche stehen zur Verfügung
18.11.08: Die Folien zur heutigen Vorlesung und zur Vorlesung der letzten Woche stehen zur Verfügung
04.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung
29.10.08: Die Folien zur Vorlesung am 28.10.08 stehen zur Verfügung
27.10.08: Nachdem die Vorlesung in der ersten Woche wegen Krankheit ausgefallen ist, findet sie erstmals morgen, am 28.10.08, statt
24.09.08: Webseite angelegt.
Termine
- Vorlesung: Dienstags, 16:15 - 17:45 Uhr, Raum B016
- Übung: Mittwochs, 18:00 - 19:30 Uhr, Raum B016
Terminplan
Dienstag
|
Mittwoch
|
21.10.08: Vorlesung
|
22.10.08: Übung |
| 28.10.08: Vorlesung |
29.04.08: Übung |
| 04.11.08: Vorlesung |
05.11.08: Übung |
| 11.11.08: Vorlesung |
12.11.08: Übung |
| 18.11.08: Vorlesung |
19.11.08: Übung |
| 25.11.08: Vorlesung |
26.11.08: Übung |
| 02.12.08: --- |
03.12.08: --- |
| 09.12.08: Vorlesung |
10.12.08: Übung |
| 16.12.08: Vorlesung |
17.12.08: Vorlesung |
| 06.01.09: Vorlesung |
07.01.09: Übung |
| 13.01.09: Vorlesung |
14.01.09: Übung |
| 20.01.09: Vorlesung |
21.01.09: Übung |
| 27.01.09: --- |
28.01.09: --- |
| 03.02.09: Vorlesung |
04.02.09: Übung |
| 10.02.09: Vorlesung |
11.02.09: Übung |
Materialien
Folien und andere Materialien werden hier jeweils nach der Vorlesung/Übung bereitgestellt.
Folien
-
01intro.pdf
- Introduction and Motivation (Vorlesung am 28.10.08)
-
02semiFormalSpecification.pdf
- Semi-formal Specification (Vorlesung am 04.11.08)
-
03unitSpecification.pdf
- Unit Specification (Vorlesung am 04.11.08)
-
04JML.pdf
- Java Modeling Language (Vorlesung am 11.11.08)
-
05OCL.pdf
- Object Contraint Language (Vorlesung am 18.11.08)
-
06OCL-bsp.pdf
- Object Contraint Language, Beispiele (Übung am 19.11.08)
-
07ASMs.pdf
- Abstract State Machines (Vorlesung am 25.11.08 bis Folie 22, Vorlesung am 9.12.08 ab Folie 23)
-
08ASMs-bsp.pdf
- Abstract State Machines, Beispiel Steam Boiler (Übung am 10.12.08)
- GENTLE.pdf - Das Tutorial zur Common Algebraic Specification Language (Vorlesung am 17.12.08). Einführung dazu: Kompaktheitssatz, Grenzen der Ausdruckskraft der Prädikatenlogik und ihre Bedeutung für die formale Spezifikation (Vorlesung am 16.12.08). Weitere Informationen zu CASL gibt es auf der Webseite der CoFI
CASLTrees.pdf - Beispiel: Algebraische Spezifikation der Datenstruktur Trees
- 10Z.pdf
- Die Spezifikationssprache Z (Vorlesungen am 06.01., 13.01. und 20.01.09)
- 11LTL.pdf
- Lineare Temporale Logik (LTL)
- 12LTLmodelChecking.pdf
- LTL Model Checking
Zielgruppe
Die Vorlesung richtet sich vorwiegend an Studierende der
Bachelor-Studiengänge, sie kann aber auch in den Diplom-Studiengängen eingebracht werden.
Inhalt
Diese Veranstaltung soll die Studierenden in die Lage versetzen, formale Spezifikationssprachen zu verstehen, Spezifikationen lesen und selbst erstellen zu können.
- Design by Contract
- Invarianten, Vor- und Nachbedingungen
- Object Constraint Language (OCL)
- Java Modelling Language (JML)
- State Charts
- Abstrakte Datentypen
Bernhard Beckert