Prof. Dr. Manfred Schmidt-Schauß Fachbereich Informatik (20) Künstliche Intelligenz/Softwaretechnologie Johann Wolfgang Goethe-Universität Frankfurt am Main

Funktionale Programmieren II:

Semantik, statische Analyse, Verifikation und abstrakte Interpretation

Wintersemester 1996/97

Übungsblatt Nr. 1

This is so cool. I always knew Windows 95 was com-

plete shit, but … aus Stephen Fry: Making History

Aufgabe 1

Betrachten sie folgendes Programm:

X:=(while true do Skip)∨ true

Es sei σ_{0} die Substitution, die für alle Speicherplätze undefiniert ist.

a) Leiten sie σ′ ab, wobei:

⟨X:=(while true do Skip)∨ true,σ_{0}⟩ → σ′.

Auf welches Problem stößt ein Interpretierer für IMP?

b) Wie verträgt sich die unter a) gemachte Beobachtung mit der Tatsache, daß IMP deterministisch ist?

Aufgabe 2

Betrachten Sie folgendes IMP-Programm P:

X:=0
if (Y<=0) then
      (X:=0,Y:=0)
     else
      (while (Y>0) X:=X+Y;Y:=Y-1)

a) Berechnen Sie σ′(X), wobei

⟨P,σ_{0}⟩ → σ′ und σ_{0}(Y) = 3.

b) Können Sie mit einfachen Schlüssen auf der operationalen Semantik zeigen, daß P äquivalent zu folgendem Programm ist:

     if (Y<=0) then
                (X:=0,Y:=0)
               else
                (X:=(Y*(Y+1))/2;Y:=0)

Aufgabe 3

In IMP sind wir gezwungen, sehr sauber zu programmieren. Ein boolscher Ausdruck kann z.B. keine Speicherzelle verändern. In Programmiersprachen wie Pascal kann man Funktionen definieren, die neben ihren eigentlichen Wert auch noch Seiteneffekte in Form von Speicherveränderungen zulassen. Wir wollen dieses auch in IMP einführen, sprich boolsche Ausdrücke, die Befehle enthalten, zulassen. Ändern Sie hierzu die Syntax von IMP und zeigen Sie an ausgewählten Regeln, wie die operationale Semantik anzupassen ist.

Aufgabe

Wie muß die Operationale Semantik erweitert werden, wenn wir in IMP auch noch Labels und GoTo-Anweisungen einführen. (Bitte nur kurz erläutern!)