Beweise uber Datenstrukturen

mit dem KIV-Kalkul:

Simplifier und Heuristiken

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 57 / 290

KIV-Kalkul: Uberblick

• Versuch 1: Basisregeln, ab Versuch 2: KIV-Kalkul

• Wechseln durch”Use Basic Rules“ unter Menu Control-Options

• Sequenzenkalkul kennt keine Beweisstrukturierung:⇒ Lemmas + Regeln zum Anwenden von Lemmas

• Beobachtung: Sequenzenkalkul ist sehr elementar:⇒ Viele Regeln automatisch anwendbar

• Deshalb: Definition eines Simplifiers, der alle unkritischen Regelnimmer automatisch anwendet.

• Regeln mit 2 Pramissen (disjunction left, conjunction right etc.) sindder Idee nach alle Fallunterscheidungen⇒ Zusammenfassen zu einer Regel case distinction

• Automatisches Anwenden von Regeln durch Heuristiken, die manjederzeit dazu- oder wegschalten kann

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 58 / 290

Spezifikation von Listen (1)

list-basic =enrich nat withsorts elem; list; constants [] : list;functions

. + . : elem × list → list;

. + . : list × list → list;

. .first : list → elem;

. .rest : list → list ;# : list → nat ;

predicates. < . : elem × elem;. ∈ . : elem × list;

variables c, b, a: elem; z2, y2, x2, z1, y1, x1, z0, y0, x0, z, y, x: list;induction list generated by [], + :: (elem × list → list);

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 59 / 290

Spezifikation von Listen (2)

axiomsirreflexivity : ` ¬ a < a; used for : s,ls;transitivity : ` a < b ∧ b < c → a < c ; used for : f,lf;totality : ` a < b ∨ a = b ∨ b < a;

constructors : `[] 6= a + x ; used for : s,ls;first : ` (a + x).first = a; used for : s,ls;rest : ` (a + x).rest = x ; used for : s,ls;

append-base : `[] + x = x ; used for : s,ls;append-rec : ` (a + x) + y = a + x + y ; used for : s,ls;

size-base : ` #([]) = 0; used for : s,ls;size-rec : ` #(a + x) = #(x) + 1; used for : s,ls;

In : ` a ∈ x ↔ (∃ y , z . x = y + a + z);

end enrich

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 60 / 290

Weitere KIV-Regeln: Induktion

• Theoretisches zu Induktion spater

• In KIV gibt es pro Datentyp meist eine strukturelle Induktionsregel

• Nat. Zahlen: Wenn fur eine Formel ϕ(n)• ϕ(0) gilt• fur jedes n: aus Ind.hyp. ϕ(n) folgt: ϕ(n +1)

dann gilt fur ∀ n. ϕ(n)

• Im Sequenzenkalkul: ϕ ist jetzt die Sequenz Γ ` ∆fur Induktionsformel in Formel umwandeln!

` ϕ(0) ϕ(n) ` ϕ(n +1)

Γ ` ∆

ϕ = ∀ y .∧

Γ →∨

∆, y = free(Γ→ ∆) \ {n}

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 61 / 290

Induktion fur Listen

• Jede Liste ist entweder die leere Liste ([])oder durch Addition von a vorne an x (a + x) gebildet

• Achtung: append von zwei Listen wird auch x + y geschrieben

• Es gilt ebenfalls strukturelle Induktion:Wenn fur eine Formel ϕ(x)

• ϕ([]) gilt• Fur jede Liste x : aus Ind.hyp. ϕ(x) folgt fur jedes a: ϕ(a + x)

dann gilt fur ∀ x . ϕ(x)

` ϕ([]) ϕ(x) ` ϕ(a + x)

Γ ` ∆ϕ = ∀ y .

∧Γ →

∨∆, y = free(Γ→ ∆) \ {x}

Hinweis: Ind.hyp. weglassen entspricht Fallunterscheidung, ob Liste = []oder = a + x (≡ Regel constructor cut)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 62 / 290

Pragmatik zur Listeninduktion

• Viele Definitionen sind rekursivappend: [] + y = y , (a + x) + y = a + (x + y)size: #([]) = 0, #(a + x) = 1 + # xisprefix: isprefix([],y), ¬ isprefix(a + x ,[]),

isprefix(a + x , b + y) ↔ a = b ∧ isprefix(x , y)sorted: sorted([]), sorted(a + []),

sorted((a + (b + x)) ↔ a < b ∧ sorted(b + x)• Induktion, wann immer moglich, uber Variable am rekursiven

Argument.Also: Erstes Argument bei append und isprefix

• Wenn dort keine Variable, oft Generalisierung des Arguments zuVariable notwendig

• Anschliessend rekursive Definition anwenden (oft mit Simplifier!),dann Induktionshypothese

• Bei sorted geht Rekursion uber 2 Stufen: Induktion fur FU!

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 63 / 290

Beispiel (1)

Zu zeigen: ` # (x + y) = # x + # y

Erstes Vorkommen von x: An rekursiver Position von +Erstes Vorkommen von y: Nicht an rekursiver Position von +Zweites Vorkommen von x: An rekursiver Position von #Zweites Vorkommen von y: An rekursiver Position von #Daraus folgt: Sinnvoll fur Induktion ist nur die Variable x!

Beweis durch strukturelle Induktion uber x :Induktions Anfang x = []# ( [] + y ) = # y = 0 + # y = # x + # yInduktionsschritt x ⇒ a + x# ( (a + x) + y) = # (a + x + y) = # (x + y) + 1= # x + # y + 1 = # x + 1 + # y = # (a + x)+ # y

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 64 / 290

KIV-Kalkul: Lemmaanwendung

Beim Anwenden von Axiomen will man nicht umstandlich cut, all left(und evtl. insert equation) machen

Γ′ ` ∆′ Γ ` Θ(∧

Γ′),∆ Θ(∨

∆′),Γ ` ∆

Γ ` ∆(insert lemma)

• Γ′ ` ∆′ ist das Lemma (Axiom oder anderes Theorem)

• Θ ist eine Substitution fur die freien Variablen des Lemmas

• Die Pramisse mit dem Lemma wird vom System als geschlossenbetrachtet

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 65 / 290

KIV-Kalkul: Ersetzungslemmas

Γ′ ` ϕ → σ = τ Γ ` Θ(∧

Γ′ ∧ ϕ),∆ Γ′′ ` ∆′′

Γ ` ∆(insert rewrite lemma)

• Γ′ ` ϕ → σ = τ ist das Lemma (Γ und Vorbedingung ϕ durfenfehlen)

• Θ ist eine Substitution fur die freien Variablen des Lemmas

• Γ′′ ` ∆′′ entsteht aus Γ ` ∆ durch Ersetzen von Θ(σ) durch Θ(τ)

• Lemmas der Form Γ′ ` ϕ → (ψ ↔ χ) mit ψ Literal erlaubt:Dann wird Θ(ψ) durch Θ(χ) ersetzt

• Wird kontextsensitiv unterstutzt: Klicken auf das fuhrendeFunktionssymbol von σ in der Sequenz bietet passendeRewrite-Regeln an

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 66 / 290

KIV-Kalkul: Der Simplifier

Beobachtung: Viele Vereinfachungen macht man beim mathematischenBeweisen ohne daruber nachzudenken. Alle unkritischen Regeln wendetder Simplifier in einem Schritt immer an.

Es gibt 2 Arten von Vereinfachung:

Logische Vereinfachung

• Beipiel: Ersetzen von A ∧ A durch A (fur jede Formel A)

• Sind von Axiomen unabhangig, werden immer angewandt

Simplifierregeln

• Beispiel (nat. Zahlen): n + 0 = n zum Ersetzen von τ + 0 durch τ

• Benotigen eine als Simplifierregel markiertes Axiom oder Lemma

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 67 / 290

Simplifier: Logische Vereinfachung

• Aussagenlogische Regeln mit einer Pramisse(wie implication right, con. left, dis. right etc.)

• All right, Exists left, axiom, reflexivity

• Aussagenlogik mit true und false

• ∃ x . x = τ ∧ A kann zu Aτx vereinfacht werden, falls x 6∈ Vars(τ).

• Vereinfachung mit Hilfe des Kontexts

Beispiele:

A,ΓtrueA ` ∆true

A

A,Γ ` ∆

ΓfalseA ` A,∆false

A

Γ ` A,∆

A → BtrueA ,Γ ` ∆

A → B,Γ ` ,∆AfalseB → B,Γ ` ∆

A → B,Γ ` ,∆A ∨ B false

A ,Γ ` ∆

A ∨ B,Γ ` ∆

Γ ` A ∧ BtrueA ,∆

Γ ` A ∧ B,∆

Bsp.: A ∧ A ⇒ A ∧ AtrueA = A ∧ true ⇒ A

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 68 / 290

Simplifier: Datenstrukturabhangige Regeln

• Simplifierregeln sind Axiome oder Theoreme (Sequenzen),die einen entsprechenden Verwendungseintrag haben

• Die syntaktische Form bestimmt den Effekt

• Es gibt mehrere Klassen:• Simplifierregeln• Forward-Regeln

• Alle Regeln konnen lokal oder global sein

Zentral fur das Verstandnis von KIV:Welche Simplifierregel hat welchen Effekt?

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 69 / 290

Simplifier: Lokale und globale Regeln

2 Klassen von Simplifierregeln

• Lokale Simplifierregeln: Werden in Beweisen uber der Spezifikation,in der sie definiert sind, benutzt.

• Globale Simplifierregeln: Werden in Beweisen in Spezifikationen, dieuber der, in der sie definiert sind, benutzt.

Pragmatik

• Lokal werden Axiome als Simplifierregeln verwendet

• Global werden Theoreme verwendet, die “gute” Simplifierregeln sind

Analog fur Forward-Regeln

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 70 / 290

Simplifier: Eingabe von Simplifierregeln

Theoreme werden als Simplifierregeln eingetragen, wahlweise durch:

• Am Ende der Sequenz in der specification/sequents-Datei:used for: s, ls;

used for: f, lf;

• Auf Spezifikationsebene im Menu:Add (Local) Simplifierrules

Add (Local) Forwardrules

• Auf Spezifikationsebene: Durch Rechtsklick auf das Theoremund Anklicken der Checkbox

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 71 / 290

Simplifier: Typen von Simplifierregeln

Simplifierregeln (mit Eintrag s und/oder ls) gehoren zu einer der Klassen

• Termersetzungsregel = Rewriteregel:

Generelle Form: Γ ` ϕ → (σ = τ)Effekt: (Instanzen von) σ durch τ ersetzen

• Formelersetzungsregel = Aquivalenzregel

Generelle Form: Γ ` ϕ → (ψ ↔ χ)Effekt: (Instanzen von) ψ durch χ ersetzen

• Assoziativitat und Kommutativitat:

Generelle Form: (a + b) + c = a + (b + c) und a + b = b + aEffekt: Alle anderen Regeln modulo Ass. und Komm. anwenden

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 72 / 290

Simplifier: Pragmatik von Bedingungen

Rewrite- und Aquivalenzregeln haben die generelle Form

Γ ` ϕ → σ = τ und Γ ` ϕ → (ψ ↔ χ)

• Vorbedingungen Γ und ϕ:Als Formel dieselbe Bedeutung, aber unterschiedlich behandelt.

• ϕ = ϕ1 ∧ . . . ∧ ϕn muss Konjunktion von Literalen sein

• Literal = evtl. negierte atomare Formel

• Atomare Formel = Anwendung von Gleicheit odernicht vordefiniertem Pradikat (ungleich ∧, ∨, . . . ) auf Terme

• (Instanzen von) ϕ1, . . . , ϕn werden in Sequenz gesucht:Nichtnegierte Formeln im Antezedent, negierte im Sukzedent

• Γ wird versucht durch rekursiven Simplifieraufruf zu beweisen

• Γ darf beliebige Formeln enthalten

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 73 / 290

Simplifier: Pragmatik von Bedingungen

Wann sollte man Vorbedingungen in Γ stecken, wann in ϕ1, . . . ,ϕn?

• Vorbedingungen vor dem Sequenzenhaken in Γ sollten nur danndefiniert werden, wenn sie in sinnvollen Sequenzen immer erfullt sind.

• Typische sinnvolle Vorbedingungen sind Definiertheitsbedingungen:

• m −1 (Vorganger von m) ist nur fur m 6= 0 definiert• m − n ist nur fur n ≤ m definiert• .rest und .last sind nur fur nichtleere Listen definiert• Arrays: i < #ar sollte fur Zugriff a[i ] immer wahr sein

• Wenn man die Pragmatik nicht befolgt:Viele nutzlose Simplifieraufrufe (wird schnell sehr langsam)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 74 / 290

Simplifier: Beispiele zu Vorbedingungen

• n 6= 0 ` (m < n −1 ↔ m +1 < n)Vorbedingung ok im Antezedent, da 0 −1 nicht sinnvoll ist

• ` m < n → (n < m + 2 ↔ m + 1 = n)Nicht im Antezedent, sonst, sobald Instanzen von n < m + 2vorkommen: Viele unnotige Beweisversuche fur m < n

• m ≤ n ` (n − m) + m = m

Beweist z. B. die Sequenz f(x) > 5 ` (f(x) − 3) + 3 = f(x)(da der Simplifier f(x) > 5 ` 3 ≤ f(x) beweisen kann)

` m ≤ n → (n − m) + m = m beweist die Sequenz nicht,da 3 ≤ f(x) nicht in der Sequenz vorkommt

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 75 / 290

Simplifier: Rewrite-Regeln

Γ ` ϕ → σ = τ

ersetzt (Instanzen von) σ durch τ , wenn Vorbedingungen ok

Einschrankungen:

• free(ϕ) ∪ free(σ) muß alle freien Variablen abdecken

• σ und τ mussen Terme sein, σ darf keine Variable sein

Beispiele:

• (m + n) − n = m

• i > 0 → sqrt(i ˆ 2) = i (i integer; warum nicht im Antezedent?)

• (s1 ∪ s2) \ s2 = s1 \ s2 (Mengen)

• x 6= [] → (x + y).first = x .first (Listen, + = append, warum nichtAnt.?)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 76 / 290

Simplifier: Aquivalenzregeln

Γ ` ϕ → (ψ ↔ χ)

ersetzt (Instanzen von) ψ durch χ, wenn Vorbedingungen ok

Einschrankungen:

• free(ϕ) ∪ free(ψ) muß alle freien Variablen abdecken

• ψ muss Literal sein, χ ist beliebige Formel

• Vereinfachung: Falls ψ keine Gleichung, statt (ψ ↔ true) nur ψ

• Vereinfachung: Statt (ψ ↔ false) nur ¬ ψ

Beispiele:

• sorted(a + []), # x = 0 ↔ x = [] (Listen)

• m + n < m + n0 ↔ n < n0

• n 6= 0 ` (m < n −1 ↔ m +1 < n)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 77 / 290

Simplifier: Kommutativitat und Assoziativitat

• Kommutativitat: m + n = n + m

• Assoziativitat: (m + n) + k = n + (m + k)

• Kurz: C(+), A(+), AC(+) fur komm., ass., komm. und ass.

• Werden nicht direkt verwendet (Warum?)

• Ob eine Simplifierregel passt, wird “modulo” dieser Regeln gepruft

• ` a + b ∗ c = c ∗ b + a wird mit C(+,*) sofort (per Reflexivitat)bewiesen

• ` b ∗ c ≤ (c ∗ a) ∗ b wird fur AC(∗) mit der Regel m ≤ m ∗ nbewiesen

• Viele Operatoren sind AC: +, ∗, min, ggt, ∪• Nur assoziativ ist z. B. append auf Listen, ∗ auf Matrizen

• Nur kommutativ ist sehr selten

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 78 / 290

Simplifier: Forwardregeln

• Manchmal will man neue Information zu einer Sequenz dazunehmen

• Fast nur fur Transitivitat von Ordnungs- und Aquivalenzrelationen:• m < n ∧ n < n0 → m < n0• isperm(x , y) ∧ isperm(y , z) → isperm(x , z)

• Dazu gibt es Forward-Regeln der Form:

Γ ` ϕ1 ∧ . . . ∧ ϕn → ϕ

• Vorbedingungen werden wie bei Simplifierregeln behandelt

• ϕ wird genau einmal zur Sequenz addiert

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 79 / 290

Simplifier: Hinweise zu Forwardregeln

• Transitivitat ist unkritisch (sollte man machen)

• Haufig etliche Varianten notwendig:• m < n ∧ n ≤ n0 → m < n0• m < n ∧ ¬ n0 < n → m < n0• m ≤ n + 1 ∧ n < n0 → m ≤ n0

• Ein Lemma sollte nie Forward- und Simplifierregel sein. Warum?

• Forward-Regeln geben sehr leicht Endlosschleifen im Simplifier! ⇒Sehr vorsichtig, nur mit gutem Grund verwenden

• Einfaches Bsp. fur Endlosschleife: ` m < n → m < n + 1

• Bsp.: 0 < n ` (∗ n) ≤ m → m 6= 0

• Warum nur (∗ n) und nicht einfach n? Warum 0 < n im Antezedent?

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 80 / 290

KIV-Kalkul: Elimination fur Selektoren

• Listen haben (Postfix-)Selektoren• .first (erstes Element)• .rest (Rest der Liste)

• Trick: Selektoren loswerden mit Hilfe von insert elim lemma

• Benotigt wird Lemma` x 6= [] → (a = x .first ∧ y = x .rest ↔ x = a + y)

• Eliminationsregel sucht einen Term t.first oder t.rest

• Wenn t 6= [] gilt, wird t = a + y ersetzt (neue Variablen a, y)

• Damit wird aus t.first bzw. t.rest jetzt a bzw. y

t = a + y ,Γ(a, y , a + y) ` ∆(a, y , a + y)

t 6= [],Γ(t.first, t.rest, t) ` ∆(t.first, t.rest, t)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 81 / 290

KIV-Kalkul: Elimination fur andere Funktionen

• Manchmal geht Elimination auch fur andere “unbeliebte” Funktionen

• Beliebte Beispiele: Minus und Division

• Lemma fur Minus: n ≤ m ` n0 = m − n ↔ m = n0 + n

• Vorteil: Man kann auf Simplifierregeln fur − verzichten!

• Nachteil: Neue Variable n0 wird eingefuhrt (manchmal unintuitiv)

Γ(n0 + n, n, n0) ` ∆(n0 + n, n, n0)

n ≤ m, Γ(m, n,m − n) ` ∆(m, n,m − n)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 82 / 290

Automatisierung in KIV: Heuristiken

• Flexible Automatisierung ist zentral, um bei grossen Fallstudien nichtimmer wieder die gleichen Beweisschritte wiederholen zu mussen

• Deshalb in KIV: Automatisierung durch zuschaltbare Heuristiken

• Speziell: Der Simplifier ist eine Heuristik⇒ Sollte man (fast) immer benutzen

• Fur jedes Beweisziel werden alle Heuristiken der Reihen nachausprobiert

• Gewahlte Heuristiken jederzeit anderbar

Sehr wichtig fur das Verstandnis von KIV:Welche Heuristik hat welchen Effekt?

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 83 / 290

Wichtige Heuristiken fur PL in KIV (1)

• Simplifier• Wendet die Simplifier-Regel an

• pl case distinction• Wendet Regel case distinction an• Fur einfache bis mittelschwere Beweise• Gefahr, unnotige Fallunterscheidungen zu machen

• if-then-else-split• if-then-else-Operator:

(ϕ ⊃ σ; τ) bezeichnet σ, falls ϕ wahr ist, sonst τ• Wendet cut Regel mit ϕ an• Haufig einsetzbar, um sinnvolle Fallunterscheidungen zu erzwingen• Beispiel: Fallunterscheidung nach Anwendung von Rewrite-Regel

abs(i) = (i ≥ 0 ⊃ i ; − i)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 84 / 290

Wichtige Heuristiken fur PL in KIV (2)

• Quantifier closing• Sucht Instanzen, mit denen eine Pramisse direkt geschlossen werden

kann• Immer verwenden• Einziges Problem: Bei sehr vielen Quantoren braucht die Heuristik viel

unnotige Zeit• Deshalb Spezifikationsmethodik:

Pradikat (+ Simplifierregeln) definieren statt grosse Quantorenformelnzu verwenden

• Quantifier:• Sucht

”sinnvolle“ Instanzen fur Quantoren

• Kann Endlosschleifen verursachen!• Nur bei einfachen Quantorenbeweisen einsetzbar

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 85 / 290

Wichtige Heuristiken fur PL in KIV (3)

• structural induction:• Macht strukturelle Induktion uber “sinnvolle” Terme• Idee fur “sinnvoll”: Variablen an rekursiven Positionen:

n ist sinnvoll in m + n, da + rekursiv uber das zweite Argumentdefiniert: m + 0 = m, m + (n +1) = (m + n) +1

• Klappt meistens, aber nicht immer• Heuristik wendet ausserdem einmal die Induktionshypothese an

• module specific:• Eigentlich eine Meta-Heuristik: Erlaubt heuristische Anwendung von

Regeln durch Patterns• Pattern: Gibt Formeln (oder Schemas fur Formeln) an, die in der

Sequenz vorkommen mussen bzw. nicht vorkommen durfen + Regeldie angewandt werden soll

• Alle Patterns stehen in der Datei module-specific

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 86 / 290

Wichtige Heuristiken fur PL in KIV (4)

elimination:

• Heuristik gesteuert durch Eliminationsregeln(analog zu: Simplifier durch Simplifierregeln)

• KIV-Eingabe analog: used for: e; etc.

• Beispiel: n ≤ m ` n0 = m − n ↔ m = n0 + n

• Vorbedingung im Antezedent: n ≤ m muss beweisbar sein(analog zu Simplifierregeln)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 87 / 290

KIV-Kalkul: Heuristiksatze

• In KIV: 3 vordefinierte Heuristiksatze:• PL Heuristics: Minimale Menge sinnvoller Heuristiken• PL Heuristics + Case Splitting: Keine Induktion, FU automatisch• PL Heuristics + Struct. Ind.:

Versucht, Ziel induktiv zu beweisen und Fallunterscheidungen (FU)automatisch zu machen

• Fur grossere Projekte definiert man haufig seinen eigenenStandardsatz⇒ Datei default-heuristics

• Weitere Heuristiken fur Programme (DL). Dort noch wichtiger, daProgramme mehr Struktur haben (spater)

2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 88 / 290