Axiomatische Semantik für IMP

• Abstraktionsgrad zwischen operationaler und denotationeller Semantik

• Zweck:

– Verifikation von Programmen

– Beweis über Programmabläufe

• Idee: Annotierte Programme

C. Lüth  Korrekte Software durch Formale Methoden  23

Axiomatische Semantik: Beispiel

• Zum Beispiel Fakultät:

M:= 1;

{M = 1, N = n }

while 0 < N do M:= N* M; N:= N- 1 done

{N ≤ 0 ∧ M = n! } Axiomatische Semantik: Notation

• Vor- und Nachbedingungen:

{A}c{B}

Bedeutung: jeder Zustand, der A erfüllt, ist nach Termination von c ein Zustand, der B erfüllt.

• Partielle und totale Korrektheit.

• Zu definieren: Sprache für Vor- und Nachbedingungen (Zusicherungen), Erfüllbarkeit für Zusicherungen.

Zusicherungen

• Zusicherungen: Assn

A ::= ⊤ | ⊥ | a_{0} = a_{1} | a_{0} ≤ a_{1} | A_{0} ∧ A_{1} | A_{0} ∨ A_{1} | ¬A | A_{0} ⇒ A_{1} | ∀ i.A | ∃ i.A Arithmetische Ausdrücke Aexp erweitert um Integer-Variablen (Intvar).

• Beispiele:

– m teilt n: ∃ p. n = p ∗ m

– n Primzahl: ¬(n = 1) ∧ ∀ m. ((∃ p. n = p ∗ m) ⇒ (m = n ∨ m = 1))

• Substitution: A[a/i] (Vorsicht bei gebundenen Variablen!)

C. Lüth  Korrekte Software durch Formale Methoden  26

Semantik von Zusicherungen σ ⊧^{I} A: Zustand σ : Σ → Σ_{⊥} erfüllt Zusicherung A unter Variablenbelegung I : Intvar → ℕ.

σ ⊧^{I} ⊤ σ ⊧^{I} a_{0} = a_{1} if E[[a_{0}]]Iσ = E[[a_{1}]]Iσ σ ⊧^{I} a_{0} ≤ a_{1} if E[[a_{0}]]Iσ ≤ E[[a_{1}]]Iσ σ ⊧^{I} A ∧ B if σ ⊧^{I} A and σ ⊧^{I} B σ ⊧^{I} A ∨ B if σ ⊧^{I} A or σ ⊧^{I} B σ ⊧^{I} ¬A if not σ ⊧^{I} A σ ⊧^{I} A ⇒ B if not σ ⊧^{I} A, or σ ⊧^{I} B σ ⊧^{I} ∀ i.A if σ ⊧^{I[n/i]} A for all n ∈ ℕ σ ⊧^{I} ∃ i.A if σ ⊧^{I[k/i]} A for some k ∈ ℕ ⊥ ⊧^{I} A

C. Lüth  Korrekte Software durch Formale Methoden  27

Partielle Korrektheit und Gültigkeit formal

• Partielle Korrektheit: σ ⊧^{I} {A}c{B} ⟺ (σ ⊧^{I} A ⇒ D[[c]]σ ⊧^{I} B)

• Gültigkeit:

⊧ {A}c{B} ⟺ für alle σ, I: σ ⊧^{I} {A}c{B}

C. Lüth  Korrekte Software durch Formale Methoden  28

Hoare-Kalkül

{A}skip{A}

{A ∧ b}c_{0}{B} {A ∧ ¬b}c_{1}{B}

                         {A}if b then c_{0} else c_{1} fi{B}

{B[a/X] }X := a{B}

{A ∧ b}c{A}

                         {A}while b do c done{A ∧ ¬b}

{A}c_{0}{B} {B}c_{1}{C}
{A}c_{0}; c_{1}{C}

⊧ A ⇒ A′ {A′}c{B′} ⊧ B′ ⇒ B
{A}c{B}

C. Lüth  Korrekte Software durch Formale Methoden  29

Eigenschaften des Hoare-Kalküls

• Der Hoare-Kalkül ist konsistent: wenn ⊢ {A}c{B}, dann ⊧ {A}c{B}

• Der Hoare-Kalkül ist nicht vollständig:

wenn ⊧ {A}c{B}, dann nicht notwendigerweise ⊢ {A}c{B}.

(Gödels erster Unvollständigkeitssatz)

Weakest Precondition

Defn: Für S ∈ Com , Q ∈ Assn , I : Intvar → ℕ, die schwächste Vorbedingung wp^{I}(S, Q) ist die Zusicherung, die alle Zustände beschreibt, nach deren Ausführung S in einem Zustand terminiert, in dem Q gilt:

wp^{I}(S, Q) =^{def} {σ ∈ Σ_{⊥} | D[[S]]σ ≠ ⊥, D[[S]]σ ⊧^{I} Q }
wp(skip, Q) = Q
wp(c_{1}; c_{2}, Q) = wp(c_{1}, wp(c_{2}, Q))
wp(X := a, Q) = Q[a/X]
wp(if b then c_{1} else c_{2} fi, Q) = b ⇒ wp(c_{1}, Q) ∧ (¬b ⇒ wp(c_{2}, Q))
wp(while b do c done, Q) = ∃ k. 0 ≤ k. P_{k}
mit {P_{k} }c{P_{k+1}}

Zusammenfassung zur Semantik

• Operational: Formalisierung der Ausführung durch syntaxgesteuerte Ableitungsregeln Nützlich für Sprachdefinition, Compilerverifikation

• Denotationell: Formalisierung der Bedeutung eines Programmes durch cpo’s, IFixpunkte etc. Nützlich für Korrektheitsbeweise, Entwicklung korrekter Progr.

• Axiomatisch: Formalisierung der Ausführung und Bedeutung durch Vor- und Nachbedingungen Nützlich für Programmverifikation