Korrekte Software durch Formale Methoden

Christoph Lüth

Wintersemester 1998/99 Die Sprache IMP

• Zahlen: N = {0, 1, 2, 3, …}

• Wahrheitswerte: T = {True, False}

• Variablen: Loc

• Arithmetische Ausdrücke: Aexp a ::= n | X | a_{0} + a_{1} | a_{0} - a_{1} | a_{0} * a_{1}

C. Lüth  Korrekte Software durch Formale Methoden  2

Die Sprache IMP

• Bool’sche Ausdrücke: Bexp b ::= True | False | a_{0} = a_{1} | a_{0} <= a_{1} | not b | b_{0} and b_{1} | b_{0} or b_{1}

• Kommandos: Com

         c ::= skip | X := a | c_{0}; c_{1} | if b then c_{0} else c_{1} fi | while b do c done

C. Lüth  Korrekte Software durch Formale Methoden  3

Programming in IMP

Fac ≡ M := 1; while 0 < N do M:= N* M; N:= N- 1 done  Euclid ≡ while (not (M= N)) do if (M<= N) then N:= N- M else M:= M- N fi done

C. Lüth  Korrekte Software durch Formale Methoden  4

Semantik von IMP

• Loc bezeichnet symbolische Adressen

• Systemzustand: Σ =^{def} Loc ⇀ ℕ

• Strukturelle Operationale Semantik: – Syntaxgesteuerte Auswertung

– Relativ zu einem Systemzustand

– Relation auf Konfigurationen: ⟨a, σ⟩

C. Lüth  Korrekte Software durch Formale Methoden  5

Operationelle Semantik von IMP: Arithmetische Ausdrücke

Zahlen:  ⟨n, σ⟩ → n
Variablen:  ⟨X, σ⟩ → σ(X)

Addition:

⟨a_{0}, σ⟩ → n ⟨a_{1}, σ⟩ → m

⟨a_{0} + a_{1}, σ⟩ → n + m

Subtraktion:

⟨a_{0}, σ⟩ → n ⟨a_{1}, σ⟩ → m

⟨a_{0} - a_{1}, σ⟩ → n − m

Multiplikation:

⟨a_{0}, σ⟩ → n ⟨a_{1}, σ⟩ → m

⟨a_{0} * a_{1}, σ⟩ → n · m

Operationelle Semantik von IMP: Bool’sche Ausdrücke

⟨True, σ⟩ → ⊤  ⟨False, σ⟩ → ⊥

{⟨b, σ⟩ → ⊥ \atop ⟨not b, σ⟩ → ⊤}  {⟨b, σ⟩ → ⊤ \atop ⟨not b, σ⟩ → ⊥}

\begin{matrix}⟨a_{0}, σ⟩ → n & ⟨a_{1}, σ⟩ → m \\ ⟨a_{0} = a_{1}, σ⟩ → ⊤ \end{matrix} if n = m \begin{matrix}⟨a_{0}, σ⟩ → n & ⟨a_{1}, σ⟩ → m \\ ⟨a_{0} = a_{1}, σ⟩ → ⊥ \end{matrix} if n ≠ m

\begin{matrix}⟨a_{0}, σ⟩ → n & ⟨a_{1}, σ⟩ → m \\ ⟨a_{0} <= a_{1}, σ⟩ → ⊤ \end{matrix} if n ≤ m \begin{matrix}⟨a_{0}, σ⟩ → n & ⟨a_{1}, σ⟩ → m \\ ⟨a_{0} <= a_{1}, σ⟩ → ⊥ \end{matrix} if n > m

\begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊥ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊥ \end{matrix}

\begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊥ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊤ \end{matrix}

\begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊤ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊤ \end{matrix}

\begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊤ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊥ \end{matrix}

Operationelle Semantik von IMP: Bool’sche Ausdrücke sequentiell

{⟨b_{0}, σ⟩ → ⊥ \atop ⟨b_{0} and b_{1}, σ⟩ → ⊥}

\begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊥ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊤ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} and b_{1}, σ⟩ → ⊤ \end{matrix}

{⟨b_{0}, σ⟩ → ⊤ \atop ⟨b_{0} or b_{1}, σ⟩ → ⊤}

\begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊤ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊤ \end{matrix}  \begin{matrix}⟨b_{0}, σ⟩ → ⊥ & ⟨b_{1}, σ⟩ → ⊥ \\ ⟨b_{0} or b_{1}, σ⟩ → ⊥ \end{matrix}

C. Lüth  Korrekte Software durch Formale Methoden  9

Operationelle Semantik von IMP: Anweisungen ⟨skip, σ⟩ → σ

{⟨a, σ⟩ → n \atop ⟨X := a, σ⟩ → σ[n/X]}  \begin{matrix}⟨c_{0}, σ⟩ → τ & ⟨c_{1}, τ⟩ → τ′ \\ ⟨c_{0}; c_{1}, σ⟩ → τ′ \end{matrix}
⟨b, σ⟩ → ⊤ ⟨c_{0}, σ⟩ → τ

⟨if b then c_{0} else c_{1} fi, σ⟩ → τ

⟨b, σ⟩ → ⊥ ⟨c_{1}, σ⟩ → τ

                               ⟨if b then c_{0} else c_{1} fi, σ⟩ → τ

⟨b, σ⟩ → ⊥

⟨while b do c done, σ⟩ → σ

⟨b, σ⟩ → ⊤ ⟨c, σ⟩ → τ′ ⟨while b do c done, τ′⟩ → τ

            ⟨while b do c done, σ⟩ → τ

C. Lüth  Korrekte Software durch Formale Methoden  10

Beweisprinzipien • Induktion über Herleitung

• Strukturelle Induktion über Termaufbau.

• Wohlfundierte Induktion (Noether’sche Induktion): Relation ≺⊂ X ×X ist wohlfundiert wenn es keine unendlichen absteigenden Ketten x_{0} ≺ x_{1} ≺ x_{2} ≺ x_{3} ≺ … gibt oder jede nichtleere Teilmenge Q ⊆ X hat ein minimales Element. Wohlfundierte Induktion:

∀ x ∈ X.P(x) ⟺ ∀ x.(∀ y ≺ x.P(y)) ⇒ P(x)

C. Lüth  Korrekte Software durch Formale Methoden  11

Erweiterung von IMP: TINY • TINY: Ein/Ausgabe, Fehlerbehandlung.

• Systemzustand:

Σ =^{def} Mem × ℕ^{∗} × ℕ^{∗}
Mem =^{def} Loc ⇀ (ℕ + {u})

• Auswertung: ⟨c, σ⟩ → Σ + {e}

• Zusätzliche Regeln für Fehlerpropagation, Eingabe, Ausgabe.

C. Lüth  Korrekte Software durch Formale Methoden  12