Bereich: I, 2+1 SWS.

Zeit und Ort: Montag 12:30 - 14:00 in 0606. Beginn: 3.5.

Zentralübung: Vierzehntägig Dienstag 14 - 16 in 2760. Beginn: 18.5.
Aufgrund der Pfingstferien finden am 25.05 und am 01.06 keine Uebungen statt!
Übungsleitung: Max Breitling und Jan Philipps.

Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt, und in der Zentralübung behandelt.

Lösungsvorschläge werden nur in der Zentralübung besprochen, und können leider nicht schriftlich bereitgestellt werden. Bei Bedarf werden in der Vorlesung auch Arbeits- und Merkblätter ausgeteilt.

Inhalt der Vorlesung:

1. Modellorientierte Spezifikationen mit Z
1. Das Unix Dateisystem in Z
2. Funktionale Datentypverfeinerung in Z. Beispiel: Implementierung von Mengen von Listen durch sogenannte "Tries".
3. Datentypverfeinerung mit Simulationsrelationen. Beispiel: Speicherverwaltung. Grenzen der (vorwärts) Simulation: interner Nichtdeterminismus. Beispiel: Kinokassen.
2. UML und OCL
1. Überblick über die Unified Modelling Language
2. Klassendiagramme: Klassen, Attribute, Methoden, Vererbung, Assoziationen.
3. Die Object Constraint Language: Klasseninvarianten, Navigationsausdrücke, Kollektionstypen, Standardfunktionen über Kollektionen, Vor- und Nachbedingungen für Methoden.
3. Input/Output Automaten
   1. Klassifikation paralleler Systeme: Synchron, asynchron (sowohl bzgl Zeit als auch Kommunikation), gemeinsamer Speicher, Nachrichten. Beispiel: Cola-Automat und Mensch.
   2. Formalisierung von IOA.
   3. Invarianten. Beispiel: Quadratwurzelberechnung ohne Multiplikation.
   4. Parallele Komposition. Beispiel: Leader Election in einem Ring von Prozessen.
   5. Automatenverfeinerung mit Abstraktionsfunktionen. Beispiel: Das Alternating Bit Protokoll. Beweis mit Verifikationsdiagramm.
   6. Vollständigkeit der Automatenverfeinerung: Vorwärts-Simulation, Rückwärts-Simulation, und die Vollständigkeit der Kombination der beiden Simulationen.
4. Hoare-logik für parallele Programme
   1. Motivierende Beispiele
   2. Disjunkter Parallelismus und die Notwendigkeit von Hilfsvariablen.
   3. Die Methode von Owicki und Gries.

Voraussetzungen: Grundlagen der Programm- und Systementwicklung I

Empfehlenswert für: Grundlage für Programmierung und Software Engineering

Übungsschein/Klausur: Am Ende des Sommersemesters wird auf Wunsch eine Semestralklausur zum Stoff der Vorlesung und der Übungen stattfinden. Studentinnen und Studenten, die an dieser Klausur teilnehmen möchten, müssen sich verbindlich anmelden. Nach Abschluß des Sommersemesters wird allen Studentinnen und Studenten, die die angebotene Klausur bestanden haben, ein Übungsschein ausgestellt.

Sprechstunde: Mittwoch 12-13 im Raum -2550 (Dienstzimmer von Prof. Nipkow)
 

Literatur:

Noch ein Buch zu Z:

• J. C. P. Woodcock und J. Davies. Using Z: Specification, Proof and Refinement. 1996.

Input/Autput Automaten und verteilte Algorithmen:

• Nancy Lynch and Mark Tuttle. An Introduction to Input/Output Automata. CWI Quarterly 2(3):219-246, September 1989.
• Nancy Lynch. Distributed Algorithms. Morgan Kaufmann, 1998.

Hoare Logik für parallele Programme:

• Apt und Olderog. Programmverifikation. Sequentielle, parallele und verteilte Programme. Springer Verlag, 1994.

Und etwas zu UML und OCL:

• Martin Fowler und Kendall Scott. UML Distilled : Applying the Standard Object Modeling Language. Addison-Welsey, 1997.
• Jos B. Warmer   und Anneke G. Kleppe. The Object Constraint Language : Precise Modeling with UML. Addison-Wesley, 1999.
• Bernd Oestereich. Objektorientierte Softwareentwicklung mit der Unified Modeling Language. R. Oldenbourg Verlag München, 1997.
• Grady Booch, James Rumbaugh und Ivar Jacobson. The Unified Modeling Language - User Guide. Addison-Wesley, 1998.