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. 2

J.L.: Are we supposed to giggle in the solo? P.M.: Yeah!

aus The Beatles: Anthology 3

Aufgabe 1

Wir wollen für diese Aufgabe IMP etwas abändern zu IMPTB. Statt der ganzen Zahlen und boolscher Konstanten sind in IMPTB nur noch die Zahlen 0 und 1 als Konstanten enthalten. Wir geben die neue operationale Semantik für das geänderte IMP soweit für diese Aufgabe notwendig an:

arithmetische und boolsche Ausdrücke:

• \frac{⟨a_{1},σ⟩→0 ⟨a_{2},σ⟩→n_{2}}{⟨a_{1}⊗a_{2},σ⟩→0}
• \frac{⟨a_{1},σ⟩→n_{1} ⟨a_{2},σ⟩→0}{⟨a_{1}⊗a_{2},σ⟩→0}
• \frac{⟨a_{1},σ⟩→1 ⟨a_{2},σ⟩→1}{⟨a_{1}⊗a_{2},σ⟩→1}

für ⊗ ∈ {+, −, ∗, ≤, =, ≥, <, >}

Befehle:

• \frac{⟨b,σ⟩→0}{⟨if b then c_{1} else c_{2},σ⟩→σ_{0}} , mit σ_{0} X = 0 für alle X.

• \frac{⟨b,σ⟩→1 ⟨c_{1},σ⟩→σ′}{⟨if b then c_{1} else c_{2},σ⟩→σ′}
• \frac{⟨b,σ⟩→1 ⟨c_{2},σ⟩→σ′}{⟨if b then c_{1} else c_{2},σ⟩→σ′}

a) Welche Eigenschaft von IMP hat IMPBT nicht?

b) Definieren Sie sinnvolle Regeln für die operationale Semantik von while für IMPBT?

c) Betrachten sie folgendes Programm P:

Ak:=0; N :=1; while (N > 1) do (Ak:= (Ak∗1);N:=N−1))

Leiten sie in der operationalen Semantik σ′ her für: ⟨P, σ⟩ → σ′

d) Wir wollen eine denotationale Semantik für IMPBT aufbauen. Hierzu stellen wir Umgebungen als Tupel der Werte aller globalen Variablen dar. Nichtinitialisierte Speicherplätze werden dabei immer mit 0 belegt. Wir definieren eine Relation für die Tupelumgebungen durch: (v_{1}, …, v_{n}) ≥ (v′_{1}, …, v′_{n}) gdw. für alle i : v_{i} ≥ v′_{i}. Es gilt dabei: 0 ≥ 0, 1 ≥ 1, 1 ≥ 0. In üblicher Weise gelte: x > y gdw.: x ≥ y und nicht y ≥ x.

Für if sei die denotationale Semantik von IMP gegeben durch:

– C[[if b then c_{1} else c_{2}]] = λ(v_{1}, …, v_{n}).(0, …, 0) für C[[b]](v_{1}, …, v_{n}) = 0

– C[[if b then c_{1} else c_{2}]] = λ(v_{1}, …, v_{n}).(C[[c_{1}]](v_{1}, …, v_{n}) ⊔ C[[c_{2}]](v_{1}, …, v_{n})) für C[[b]](v_{1}, …, v_{n}) = 1

wobei ⊔ die kleinste obere Schranke in der obigen Ordnung auf Tupeln bezeichnet.

Versuchen Sie, die operationale Semantik von IMPBT in schlüssiger Weise weiterzudefinieren. Hierbei ist natürlich insbesondere while interessant.

e) Leiten Sie den denotationalen Wert von P her.