Beweise uber Datenstrukturen mit dem KIV-Kalk ul: Simpli ... · Beweise uber Datenstrukturen mit...

of 32/32
Beweise ¨ uber Datenstrukturen mit dem KIV-Kalk¨ ul: Simplifier und Heuristiken 2. Mai 2013 G. Schellhorn, D. Haneberg: Formale Methoden im Software Engineering 57 / 290
  • date post

    15-Oct-2019
  • Category

    Documents

  • view

    1
  • download

    0

Embed Size (px)

Transcript of Beweise uber Datenstrukturen mit dem KIV-Kalk ul: Simpli ... · Beweise uber Datenstrukturen mit...

  • Beweise über Datenstrukturen

    mit dem KIV-Kalkül:

    Simplifier und Heuristiken

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

  • KIV-Kalkül: Überblick

    • Versuch 1: Basisregeln, ab Versuch 2: KIV-Kalkül• Wechseln durch

    ”Use Basic Rules“ unter Menü Control-Options

    • Sequenzenkalkül kennt keine Beweisstrukturierung:⇒ Lemmas + Regeln zum Anwenden von Lemmas

    • Beobachtung: Sequenzenkalkül ist sehr elementar:⇒ Viele Regeln automatisch anwendbar

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

    • Regeln mit 2 Prämissen (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 später• In KIV gibt es pro Datentyp meist eine strukturelle Induktionsregel• Nat. Zahlen: Wenn für eine Formel ϕ(n)

    • ϕ(0) gilt• für jedes n: aus Ind.hyp. ϕ(n) folgt: ϕ(n +1)

    dann gilt für ∀ n. ϕ(n)• Im Sequenzenkalkül: ϕ ist jetzt die Sequenz Γ ` ∆

    für 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 für 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 für eine Formel ϕ(x)• ϕ([]) gilt• Für jede Liste x : aus Ind.hyp. ϕ(x) folgt für jedes a: ϕ(a + x)

    dann gilt für ∀ 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 möglich, über 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 über 2 Stufen: Induktion für 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 für Induktion ist nur die Variable x!

    Beweis durch strukturelle Induktion über 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-Kalkül: Lemmaanwendung

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

    Γ′ ` ∆′ Γ ` Θ(∧

    Γ′),∆ Θ(∨

    ∆′),Γ ` ∆Γ ` ∆ (insert lemma)

    • Γ′ ` ∆′ ist das Lemma (Axiom oder anderes Theorem)• Θ ist eine Substitution für die freien Variablen des Lemmas• Die Prämisse mit dem Lemma wird vom System als geschlossen

    betrachtet

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

  • KIV-Kalkül: Ersetzungslemmas

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

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

    Γ ` ∆(insert rewrite lemma)

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

    • Θ ist eine Substitution für die freien Variablen des Lemmas• Γ′′ ` ∆′′ entsteht aus Γ ` ∆ durch Ersetzen von Θ(σ) durch Θ(τ)• Lemmas der Form Γ′ ` ϕ → (ψ ↔ χ) mit ψ Literal erlaubt:

    Dann wird Θ(ψ) durch Θ(χ) ersetzt

    • Wird kontextsensitiv unterstützt: Klicken auf das führendeFunktionssymbol von σ in der Sequenz bietet passendeRewrite-Regeln an

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

  • KIV-Kalkül: Der Simplifier

    Beobachtung: Viele Vereinfachungen macht man beim mathematischenBeweisen ohne darüber 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 (für jede Formel A)• Sind von Axiomen unabhängig, werden immer angewandt

    Simplifierregeln

    • Beispiel (nat. Zahlen): n + 0 = n zum Ersetzen von τ + 0 durch τ• Benötigen 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 Prämisse(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 ` ∆trueAA,Γ ` ∆

    ΓfalseA ` A,∆falseAΓ ` A,∆

    A → BtrueA ,Γ ` ∆A → B,Γ ` ,∆

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

    A ∨ B falseA ,Γ ` ∆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: Datenstrukturabhängige 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 können lokal oder global sein

    Zentral für das Verständnis 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 über der Spezifikation,in der sie definiert sind, benutzt.

    • Globale Simplifierregeln: Werden in Beweisen in Spezifikationen, dieüber der, in der sie definiert sind, benutzt.

    Pragmatik

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

    Analog für 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 Menü: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) gehören zu einer der Klassen

    • Termersetzungsregel = Rewriteregel:

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

    • Formelersetzungsregel = Äquivalenzregel

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

    • Assoziativität und Kommutativität:

    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 Äquivalenzregeln 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 oder

    nicht vordefiniertem Prädikat (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 erfüllt sind.

    • Typische sinnvolle Vorbedingungen sind Definiertheitsbedingungen:• m −1 (Vorgänger von m) ist nur für m 6= 0 definiert• m − n ist nur für n ≤ m definiert• .rest und .last sind nur für nichtleere Listen definiert• Arrays: i < #ar sollte für 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 unnötige Beweisversuche für 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

    Einschränkungen:

    • free(ϕ) ∪ free(σ) muß alle freien Variablen abdecken• σ und τ müssen 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 nicht

    Ant.?)

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

  • Simplifier: Äquivalenzregeln

    Γ ` ϕ → (ψ ↔ χ)

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

    Einschränkungen:

    • 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: Kommutativität und Assoziativität

    • Kommutativität: m + n = n + m• Assoziativität: (m + n) + k = n + (m + k)• Kurz: C(+), A(+), AC(+) für komm., ass., komm. und ass.• Werden nicht direkt verwendet (Warum?)• Ob eine Simplifierregel passt, wird “modulo” dieser Regeln geprüft• ` a + b ∗ c = c ∗ b + a wird mit C(+,*) sofort (per Reflexivität)

    bewiesen

    • ` b ∗ c ≤ (c ∗ a) ∗ b wird für 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 für Transitivität von Ordnungs- und Äquivalenzrelationen:

    • 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

    • Transitivität ist unkritisch (sollte man machen)• Häufig 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. für 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-Kalkül: Elimination für Selektoren

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

    • Trick: Selektoren loswerden mit Hilfe von insert elim lemma• Benötigt 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-Kalkül: Elimination für andere Funktionen

    • Manchmal geht Elimination auch für andere “unbeliebte” Funktionen• Beliebte Beispiele: Minus und Division• Lemma für Minus: n ≤ m ` n0 = m − n ↔ m = n0 + n• Vorteil: Man kann auf Simplifierregeln für − verzichten!• Nachteil: Neue Variable n0 wird eingeführt (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 müssen

    • Deshalb in KIV: Automatisierung durch zuschaltbare Heuristiken• Speziell: Der Simplifier ist eine Heuristik⇒ Sollte man (fast) immer benutzen

    • Für jedes Beweisziel werden alle Heuristiken der Reihen nachausprobiert

    • Gewählte Heuristiken jederzeit änderbar

    Sehr wichtig für das Verständnis von KIV:Welche Heuristik hat welchen Effekt?

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

  • Wichtige Heuristiken für PL in KIV (1)

    • Simplifier• Wendet die Simplifier-Regel an

    • pl case distinction• Wendet Regel case distinction an• Für einfache bis mittelschwere Beweise• Gefahr, unnötige Fallunterscheidungen zu machen

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

    (ϕ ⊃ σ; τ) bezeichnet σ, falls ϕ wahr ist, sonst τ• Wendet cut Regel mit ϕ an• Häufig 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 für PL in KIV (2)

    • Quantifier closing• Sucht Instanzen, mit denen eine Prämisse direkt geschlossen werden

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

    unnötige Zeit• Deshalb Spezifikationsmethodik:

    Prädikat (+ Simplifierregeln) definieren statt grosse Quantorenformelnzu verwenden

    • Quantifier:• Sucht

    ”sinnvolle“ Instanzen für 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 für PL in KIV (3)

    • structural induction:• Macht strukturelle Induktion über “sinnvolle” Terme• Idee für “sinnvoll”: Variablen an rekursiven Positionen:

    n ist sinnvoll in m + n, da + rekursiv über 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 für Formeln) an, die in der

    Sequenz vorkommen müssen bzw. nicht vorkommen dürfen + 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 für 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-Kalkül: Heuristiksätze

    • In KIV: 3 vordefinierte Heuristiksätze:• 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

    • Für grössere Projekte definiert man häufig seinen eigenenStandardsatz⇒ Datei default-heuristics

    • Weitere Heuristiken für Programme (DL). Dort noch wichtiger, daProgramme mehr Struktur haben (später)

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