Warum Denotationelle Semantik?

• Abstraktere Betrachtung:

Wenn c_{1} ∼ c_{2}, dann “gleiche Bedeutung”

• Programme in verschiedenen Programmiersprachen vergleichen

• Kompositionalität und referentielle Transparenz:

D[[ϕ(e_{1}, …, e_{n}) ]] = Φ(D[[e_{1}]], …, D[[e_{n} ]])

C. Lüth  Korrekte Software durch Formale Methoden  13

Denotationelle Semantik • Programme werden durch Funktionen denotiert.

• Semantische Funktionen ordnen Kommandos und Ausdrücken Bedeutungen zu:

Arith. Ausdrücke  E : Aexp → (Σ → ℕ)
Boolsche Ausdrücke  B : Bexp → (Σ → 𝔹)
Kommandos  D : Com → (Σ ⇀ Σ)

• Programme = Partielle Funktion auf Zuständen

C. Lüth  Korrekte Software durch Formale Methoden  14

Denotationelle Semantik von IMP: Arithmetische Ausdrücke

E[[n]] =^{def} λ σ ∈ Σ.n
E[[X]] =^{def} λ σ ∈ Σ.σ(X)
E[[a_{0} + a_{1}]] =^{def} λ σ ∈ Σ.(E[[a_{0}]]σ + E[[a_{1}]]σ)
E[[a_{0} - a_{1}]] =^{def} λ σ ∈ Σ.(E[[a_{0}]]σ − E[[a_{1}]]σ)
E[[a_{0} * a_{1}]] =^{def} λ σ ∈ Σ.(E[[a_{0}]]σ · E[[a_{1}]]σ)

Denotationelle Semantik von IMP: Boolsche Ausdrücke

B[[True]] =^{def} λ σ ∈ Σ.⊤
B[[False]] =^{def} λ σ ∈ Σ.⊥
B[[not b]] =^{def} λ σ ∈ Σ.¬B[[b]]σ
B[[a_{0} = a_{1}]] =^{def} λ σ ∈ Σ. \{ \begin{matrix}⊤ & falls E[[a_{0}]]σ = E[[a_{1}]]σ \\ ⊥ & falls E[[a_{0}]]σ ≠ E[[a_{1}]]σ \end{matrix}

B[[a_{0} <= a_{1}]] =^{def} λ σ ∈ Σ. \{ \begin{matrix}⊤ & falls E[[a_{0}]]σ ≤ E[[a_{1}]]σ \\ ⊥ & falls E[[a_{0}]]σ > E[[a_{1}]]σ \end{matrix}
B[[b_{0} and b_{1}]] =^{def} λ σ ∈ Σ.B[[b_{0}]]σ ∧ B[[b_{1}]]σ
B[[b_{0} or b_{1}]] =^{def} λ σ ∈ Σ.B[[b_{0}]]σ ∨ B[[b_{1}]]σ

C. Lüth  Korrekte Software durch Formale Methoden  16

Complete Partial Orders I

• Defn: Eine partielle Ordnung ⊑ auf einer Menge X ist – transitiv: x ⊑ y, y ⊑ z ⇒ x ⊑ z

– reflexiv: x ⊑ x

– antisymmetrisch: x ⊑ y, y ⊑ x ⇒ x = y

• Defn: Für Y ⊆ X, die kleinste oberste Schranke ⨆ Y ∈ X ist: – ∀ y ∈ Y .y ⊑ ⨆ Y

– ∀ z ∈ X.(∀ y ∈ Y .y ⊑ z) ⇒ ⨆ Y ⊑ Z

C. Lüth  Korrekte Software durch Formale Methoden  17

Complete Partial Orders II

• Defn: Eine partielle Ordnung ⊑ ist vollständig (complete, cpo) wenn für jede ω-Kette x_{1} ⊑ x_{2} ⊑ x_{3} ⊑ x_{4} … = {x_{i} | i ∈ ω} eine kleinste oberste Schranke ⨆_{i∈ω} x_{i} existiert.

Ein cpo heißt spitz (pointed, pcpo), wenn es ein kleinstes Element ⊥ ∈ X gibt.

• Defn: Seien (X, ⊑) und (Y , ≤) cpo’s. Eine Funktion f : X → Y ist

– monoton wenn x ⊑ y ⇒ f (x) ≤ f (y)

– stetig wenn monoton und f ⨆_{i∈ω} x_{i} = ⨆_{i∈ω} f (x_{i})

Fixpunkte

• Satz: Sei (X, ⊑) ein pcpo, und f : X → X stetig, dann hat f einen kleinsten IFixpunkt fix(f ), gegeben durch

fix(f ) = ⨆_{n∈ω} f^{n}(⊥)

• Σ als pcpo Σ_{⊥} mit neuem Element, geordnet als ⊥ ⊑ σ. Modelliert partielle Funktionen:

Σ ⇀ Σ ≅ Σ → Σ_{⊥}

Σ → Σ_{⊥} ist ein pcpo, geordnet als

f ⊑ g ⟺ ∀ x.f (x) ⊑ g(x)

Denotationelle Semantik von IMP: Kommandos

D[[skip]] =^{def} λ σ ∈ Σ.σ
D[[X := a]] =^{def} λ σ ∈ Σ.σ[E[[a]]σ/X]
D[[c_{0}; c_{1} ]] =^{def} D[[c_{1}]] ∘ D[[c_{0}]]
D[[if b then c_{0} else c_{1} fi]] =^{def} λ σ ∈ Σ. \{ \begin{matrix}D[[c_{0}]]σ & falls B[[b]]σ = ⊤ \\ D[[c_{1}]]σ & falls B[[b]]σ = ⊥ \end{matrix}

D[[while b do c done]] =^{def} fix(Γ)
mit Γ(ϕ) =^{def} λ σ ∈ Σ. \{ \begin{matrix}ϕ ∘ D[[c]]σ & falls B[[b]]σ = ⊤ \\ σ & falls B[[b]]σ = ⊥ \end{matrix}

C. Lüth  Korrekte Software durch Formale Methoden  20

Äquivalenz von operationeller und denotationeller Semantik

• Lemma: Für a ∈ Aexp , n ∈ ℕ, E[[a]]σ = n ⟺ ⟨a, σ⟩ → n Beweis: Strukturelle Induktion über a

• Lemma: Für b ∈ BExp , t ∈ 𝔹, B[[b]]σ = t ⟺ ⟨b, σ⟩ → t Beweis: Strukturelle Induktion über b

• Lemma: Für c ∈ Com , ⟨c, σ⟩ → σ′ ⇒ D[[c]]σ = σ′ Beweis: Induktion über der Herleitung von ⟨c, σ⟩ → σ′.

• Satz (Äquivalenz der Semantiken): Für c ∈ Com , und σ, σ′ ∈ Σ,

⟨c, σ⟩ → σ′ ⟺ D[[c]]σ = σ′

Beweis: Strukturelle Induktion über c mit IFixpunktinduktion für die Iteration.

• IFixpunktinduktion: Für pcpo (X, ⊑), f : X → X stetig und P ⊆ X: – P inklusiv: wenn x_{i} ∈ P für alle i ∈ ω, dann ⨆_{i∈ω} x_{i} ∈ P

– ⊥ ∈ P, x ∈ P ⇒ f (x) ∈ P dann fix(f ) ∈ P.

C. Lüth  Korrekte Software durch Formale Methoden  22