Grundlagen der Programmierung : Semantik und Verifikation

Aktuelles

14.02.99. Blatt 11: Ab Schachtelungstiefe 12 in Beweisen kommt eine Fehlermeldung Integer too long. Hier handelt es sich um einen BUG. Wird bald behoben. Momentan solche Schachtelungstiefen vermeiden (Aufgabenstellung läßt dies zu!

20.01.99. Blatt 7, Aufgabe 31 war zudem noch ein Tippfehler: x <= y musste x < y heissen. (korrigiert)

18.01.99. Achtung! Auf Blatt 7 wird die Definition von cpo anders verstanden als in der Vorlesung: Bitte dementsprechend aktualisierte Version des Übungsblatts erneut herunterladen! (korrigiert)

Die wish 8.0 funktioniert nicht auf allen Rechnern! Allerdings sicher auf kristall :) Notfalls mit wish -display "meinrechner:0.0" Bildschirm umlenken!

• operationale Semantik
• denotationelle Semantik
• axiomatische Semantik

Zum Beweis von Programmeigenschaften wird ein neues Werkzeug ProveEasy der Universität Edinburgh eingesetzt. ProveEasy ist ein einfacher logik-unabhängiger Beweiseditor.

Prof. Dr. Martin Wirsing

Adresse:	Raum E 0.58, Oettingenstr. 67
Telephon:	2178-2154
Email Adresse:	wirsing@informatik.uni-muenchen.de
Sprechstunde:	nach Vereinbarung

Verantwortlich für die Durchführung des Übungsbetriebs und die Aufgaben ist

Dr. Bernhard Reus

Adresse:	Raum E 05, Oettingenstr. 67
Telephon:	2178-2178
Email Adresse:	reus@informatik.uni-muenchen.de
Sprechstunde:	nach Vereinbarung

Montag     9 - 11 Uhr    Vorlesung   Raum 105, Oettingenstr. 67     BEGINN 9.11.98
Mittwoch  16 - 18 Uhr    Übung       Raum 033, Oettingenstr. 67     BEGINN 18.11.98
Freitag   12 - 14 Uhr    Vorlesung   Raum 105, Oettingenstr. 67

• H.R. Nielson, F.Nielson. Semantics with Applications. Wiley, 1992.
  einführend und vorlesungsbegleitend
• C.A. Gunter. Semantics of Programming Languages: structures and techniques. MIT Press, Foundations of Computing,1992.
  operationelle und denotationelle Semantik: einführend bis weiterführend
• V. Stoltenberg-Hansen, I. Lindstrom, E.R. Griffor. Mathematical Theory of Domains. Cambridge University Press, 1994.
  nur denotationelle Semantik: einführend bis weiterführend
• G. Winskel. The Formal Semantics of Programming Languages. MIT Press, Foundations of Computing, 1993.
  einführend bis weiterführend
• J. Loeckx, K. Sieber. The Foundations of Program Verification. Teubner/Wiley, 1984.
  einführend bis weiterführend
• K. Apt, E.-R. Olderog. Programmverifikation. Springer, 1994.
  axiomatische Semantik einführend, behandelt auch parallele Programme

Die erste Übung findet am Mittwoch, den 18.11.1998 statt. Nach dem jetzigen Stand finden die Prüfungen am Montag, dem 01.03.1999, statt.

Übungsteilnehmer

Übungsblätter

• Blatt 1
• Blatt 2
• Blatt 3 (mit Einführung ProveEasy )
  Lösungen der ProveEasy-Aufgaben
• Blatt 4 (mit Einführung ProveEasy )
  Lösungen der ProveEasy-Aufgaben
• Blatt 5 (mit Einführung ProveEasy Teil II)
  Lösungen der ProveEasy-Aufgaben
• Blatt 6
  Lösungen der ProveEasy-Aufgaben
• Blatt 7
• Blatt 8
• Blatt 9
• Blatt 10
• Blatt 11
• Blatt 12

ProveEasy zum zum Download

ProveEasy Manual (Textversion)

Hinweis: Jeder Teilnehmer an der Übung muß in der Shell einmal

install-project -add gdp

in seinem Homedirectory ausführen (und sich danach neu aus- und einloggen), damit er in die Gruppe gdp aufgenommen wird. ACHTUNG: Das funktioniert momentan nur auf den alten HP-Rechnern.