Grundlagen der Programm- und Systementwicklung II
Sommersemester 1999
(Prof. Tobias Nipkow)

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.
Hörerkreis: Studenten der Informatik nach dem Vordiplom

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:


Input/Autput Automaten und verteilte Algorithmen:


Hoare Logik für parallele Programme:


Und etwas zu UML und OCL:



Olaf Müller, Max Breitling