Informelle Spezifikation

• “Entscheide, ob eine gegeben Sequenz von Elementen ein Palindrom ist.”

• “Berechne die Primfaktorzerlegung einer ganzen Zahl n ∈ ℕ”

• “Generiere in aufsteigender Reihenfolge die ersten n (n ∈ ℕ) Elemente der Sequenz aller natürlichen Zahlen, die durch keine Primzahlen außer 2, 3 und 5 teilbar sind.” (Hammings Problem)

Von der informellen zur formalen Spezifikation

• Präzisieren:

Palindrom das; Wortfolge od. Satz, die vorwärts wie rückwärts gelesen [den gleichen] Sinn ergeben, z.B. “Otto”, “Reliefpfeiler”. (Duden)

• Formalisieren und Reduktion: Sei rev eine Funktion, die Listen umdreht, dann ist

palindrom w <==> rev w = w

Spezifikation von rev

• Axiomatisch:

Erster Versuch:

rev (rev x) = x
x ~= [] ==> rev x ~= x

Zweiter Versuch:

i < length w ==> nth i w = nth (length w- i- 1) (rev w)

• Operational:

rev []     = []
rev (x#xs) = (rev xs) @ [x]

Spezifikation: Was ist zu beachten? • Notation (oben Isabelle)

• Semantik (oben Isabelle/HOL)

• Basisdatentypen (z.B. Listen)

• Programmierstil — funktional vs. imperativ

• Spezifikationsstil — algebraisch (Isabelle) vs. modellorientiert (Z)

C. Lüth  Korrekte Software durch Formale Methoden  37

Kurzwiederholung Logik I

• Syntaktische Ableitung ⊢ ϕ durch Ableitungsregeln.

• Semantische Folgerung ⊧ ϕ: ϕ gilt in allen Modellen.

• Konsistenz: ⊢ ϕ ⇒⊧ ϕ

• Vollständigkeit: ⊧ ϕ ⇒⊢ ϕ

C. Lüth  Korrekte Software durch Formale Methoden  38

Kurzwiederholung Logik II

• Gödel’s Unvollständigkeitssätze:

1. Logik L konsistent und beinhaltet Peano-Arithmetik (nat. Zahlen plus Induktionsschema) dann ist L unvollständig.

2. Logik L konsistent und beinhaltet Peano-Arithmetik dann gibt es keinen Satz ϕ, so daß ⊢ ϕ gdw L konsistent.

⇒ Nichttriviale Spezifikationssprachen sind unvollständig • Bekannte Logiken: Gleichungslogik, Horn-Logik, Aussagenlogik

und Prädikatenlogik erster Stufe (konsistent, vollständig, langweilig) Prädikatenlogik höherer Stufe (intuitionistisch, klassisch)

Kurzwiederholung Algebra

• Eine Signatur Σ = (S, Ω) besteht aus Sorten S und Operationen ω : s_{1} × … × s_{n} → s.

• Terme t ∈ T_{Σ}(X) sind entweder Variablen x ∈ X, oder eine Operation ω : s_{1} × … × s_{n} → s, angewandt auf n Terme t_{i} ∈ T_{Σ}(X)

• Eine Spezifikation SP = (Σ, R) besteht aus einer Signatur und Regeln R (Gleichungen, Ableitungsregeln, …)

• Beispiel: Monoide M = (Σ_{M}, R_{M}) Σ_{M} = ({s}, {0 :→ s, · : s × s → s } R_{M} = {0 · x = x, x · 0 = x, (x · y) · z = x · (y · z) }

Beispiel: Palindrome in Isabelle

Palindrome = List +
consts  palindrome :: 'a list => bool
defs    palindrome_def  "palindrome xs == (rev xs) = xs"
end
List = ...
consts  rev         :: 'a list => 'a list
primrec "rev([]) = []"
        "rev(x#xs) = rev(xs) @ [x]"

> use_thy "Palindrome";
Reading "Palindrome.thy"
val it = () : unit;
> goalw thy [palindrome_def] "palindrome [1,2,1,1]";
Level 0
palindrome [1, 2, 1, 1]
 1. rev [1, 2, 1, 1] = [1, 2, 1, 1]
val it = [] : thm list
>  by (Asm_simp_tac 1);
Level 1
palindrome [1, 2, 1, 1]
 1. False
val it = () : unit
>

C. Lüth  Korrekte Software durch Formale Methoden  42

> goalw thy [palindrome_def] "palindrome [2,1,2,1,2]";
Level 0
palindrome [2, 1, 2, 1, 2]
 1. rev [2, 1, 2, 1, 2] = [2, 1, 2, 1, 2]
val it = [] : thm list
> by (Asm_simp_tac 1);
Level 1
palindrome [2, 1, 2, 1, 2]
No subgoals!
val it = () : unit
>

Literature zu Isabelle: Tobias Nipkow: Isabelle — The Tutorial.

Beispiel: Palindrome in Z

[X] palindrome : ℙ seq X rev : seq X → seq X

palindrome = { w ∈ ℙ seq X | rev(w) = w } ∀ s : seq X • rev s = (λ i : 1 … #s • (#s + 1) − i) \begin{matrix}o \\ 9 \end{matrix} s