Mod - 4.51 4.3 Verifikation von Aussagen über Algorithmen Hoaresche Logik: Kalkül zum Beweisen von Aussagen über Algorithmen und Programme, Programm-Verifikation, [C.A.R. Hoare, 1969]. Statische Aussagen über Zustände (Werte von Variablen), die der Algorithmus (das Programm) an bestimmten Stellen annehmen kann, z. B. ... {pegel < max} pegel := pegel + 1; ... {0 0, y > 0; sei G größter gemeinsame Teiler von x und y Nachbedingung: a = G Algorithmus mit { Aussagen über Variable }: { G ist ggT von x und y logicaland x>0 logicaland y>0 } Terminierung der Schleife: a := x; b := y; { INV: G ist ggT von a und b logicaland a>0 logicaland b>0 } * a+b fällt monoton solange a notequal b wiederhole * a+b > 0 ist Invariante { INV logicaland a notequal b } falls a > b : { G ist ggT von a und b logicaland a>0 logicaland b>0 logicaland a>b } arrowright { G ist ggT von a-b und b logicaland a-b>0 logicaland b>0 } a := a - b { INV } sonst { G ist ggT von a und b logicaland a>0 logicaland b>0 logicaland b>a } arrowright { G ist ggT von a und b-a logicaland a>0 logicaland b-a>0 } b := b - a { INV } { INV } { INV logicaland a = b } arrowright { a = G } (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 453 Ziele: Beispiel für eine Algorithmenverifikation in der Vorlesung: Hier nur ersten Eindruck vermitteln. Später Erläuterungen * zur Konstruktionsidee, * zur Rolle der Schleifeninvarianten, * zur Anwendung der Alternativenregel, * zu Anwendungen der Zuweisungsregel * zum Terminierungsnachweis -------------------------------------------------------------------------------- Mod - 4.54 Aussage charakterisiert Programmzustände Eine Aussage P an einer Stelle in einem Algorithmus (Programm) vor oder nach einer Anweisung ... S1 {P} S2 ... charakterisiert alle Zustände, die das Programm an dieser Stelle bei irgendeiner Ausführung annehmen kann. P wird über Variable des Algorithmus formuliert. Z. B. ... { 0 lessequal i logicaland i < 10 } a[i] := 42; ... Bei jeder Ausführung liegt der Wert von i im angegebenen Intervall. Eine Aussage über andere Variablen wird hier nicht gemacht. Nur die gerade interessierende Eigenschaften der Zustände werden beschrieben. Aussagen können unterschiedlich scharf formuliert werden: { f } kein Zustand erfüllt P, Stelle nicht erreichbar { 0 lessequal i logicaland i < 2 logicaland a[i] >0 } schärfer; evtl. weniger Zustände; schwieriger zu verifizieren { 0 lessequal i logicaland i < 2 } { 0 lessequal i logicaland i < 10 } { 0 lessequal i } schwächer; evtl. mehr Zustände; leichter zu verifizieren { w } beliebige Zustände erfüllen P (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 454 Ziele: Beziehung zwischen Aussage und Zustäanden verstehen in der Vorlesung: Am Beispiel wird gezeigt: Trade-off zwischen der Schärfe der Aussage, dem Nutzen der Aussage und der Schwierigkeit sie nachzuweisen. -------------------------------------------------------------------------------- Mod - 4.55 Notation von Algorithmenelementen Anweisungsform Notation Beispiel Sequenz Anweisung1; a := x; Anweisung2 b := y Zuweisung Variable := Ausdruck a := x Alternative, zweiseitig falls Bedingung : falls a > b : Anweisung1 a := a - b sonst Anweisung2 sonst b := b - a bedingte Anweisung falls Bedingung : falls a < 0 : Anweisung1 a := - a Aufruf eines ua() berechneGgT() Unteralgorithmus ua Schleife solange Bedingung wiederhole solange anotequal b wiederhole Anweisung falls a > b : ... (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 455 Ziele: Einfache Notation von Algorithmen in der Vorlesung: 6 Anweisungsformen und ihre Schreibweise erläutern * Zuweisungszeichen := wie in Pascal (nicht wie in Java =), * Einrückung ist wichtig, um die Struktur auszudrücken * Verifikation von Aufrufen hier nur ohne Parameter, * als Anweisung kann jede der 6 Formen - auch geschachtelt - eingesetzt werden, * rekursive Definition von Anweisungsformen! Verständnisfragen: Zeigen Sie die Anwendung der Anweisungsformen am ggT-Algorithmus auf mod-3.9a -------------------------------------------------------------------------------- Mod - 4.56 Vor- und Nachbedingung von Anweisungen Aussage Q charakterisiert die Zustände, die eine Ausführung zwischen den Anweisungen A1 und A2 annehmen kann: { P } A1 { Q } A2 { R } Q ist Nachbedingung von A1 und Vorbedingung von A2 Beispiel: { i + 1 greaterequal 0} i := i + 1; { i greaterequal 0 } a [i] := k; {...} Zur Verifikation eines Algorithmus muss für jede Anweisung S ein Nachweis geführt werden: { Vorbedingung P } S { Nachbedingung Q } nachweisen: Wenn vor der Ausführung der Anweisung S die Aussage P gilt, dann gilt Q nach der Ausführung von S, falls S terminiert. Beispiel: { i + 1 greaterequal 0} i := i + 1; {i greaterequal 0} mit Zuweisungsregel nachweisen Die Aussagen werden entsprechend der Struktur von S verknüpft. Für jede Anweisungsform wird eine spezielle Schlussregel angewandt. Eine Spezifikation liefert Vorbedingung und Nachbedingung des gesamten Algorithmus: gegeben: gesucht: Aussagen über die Eingabe Aussagen über Zusammenhang zwischen Ein- und Ausgabe { Vorbedingung } Algorithmus { Nachbedingung } (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 456 Ziele: Von der Vor- zur Nachbedingung in der Vorlesung: * Zu jeder Anweisung ein Beiweisschritt * Terminierung muss separat gezeigt werden -------------------------------------------------------------------------------- Mod - 4.57 Zuweisungsregel Hoare'scher Kalkül definiert für jede Anweisungsform eine Schlussregel. Eine Zuweisung x := e wertet den Ausdruck e aus und weist das Ergebnis der Variablen x zu. { P[x/e] } x := e { P } Wenn vor der Ausführung P[x/e] gilt (P wobei x durch e substituiert ist), gilt nach der Ausführung der Zuweisung P. Beispiele: {a > 0} x := a {x > 0} {i + 1 > 0} i := i + 1 {i > 0} Wenn man zeigen will, dass nach der Zuweisung eine Aussage P für x gilt, muss man zeigen, dass vor der Zuweisung dieselbe Aussage P für e gilt. Beispiele im Algorithmus: { x>0 logicaland y>0 } a := x; { a>0 logicaland y>0 } { G ist ggT von a-b und b logicaland a-b>0 logicaland b>0 } b := y; a := a - b { a>0 logicaland b>0 } { G ist ggT von a und b logicaland a>0 logicaland b>0 } (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 457 Ziele: Zuweisungsregel verstehen in der Vorlesung: * Substitution erläutern * Vorbedingung aus der Nachbedingung rückwärts konstruieren: Was will ich zeigen? * Beispiele von Folie Mod-313a erläutern -------------------------------------------------------------------------------- Mod-4.58 Beispiele für Zuweisungsregel { P[x/e] } x := e { P } 1. { a > 0 } x := a { x > 0 } 2. { a > 0 logicaland a > 0 } x := a { x > 0 logicaland a > 0 } x durch a ersetzen - nicht umgekehrt 3. { a > 0 logicaland x = 7 } x := a { x > 0 logicaland x = 7 } falscher Schluss! alle x durch a ersetzen! 4. { a > 0 logicaland z > 0 } x := a { x > 0 logicaland z > 0 } z > 0 ist nicht betroffen 5. { i + 1 > 0 } i := i + 1 { i > 0 } 6. { i greaterequal 0} arrowboth { i + 1 > 0 } i := i + 1 { i > 0 } passend umformen 7. { i = 2 } arrowboth { i + 1 = 3 } i := i + 1 { i = 3 } passend umformen 8. { wahr } arrowboth { 1 = 1 } x := 1 { x = 1 } passend umformen 9. { z = 5 } arrowboth passend umformen { z = 5 logicaland 1 = 1 } x := 1 { z = 5 logicaland x = 1 } (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 458 Ziele: Gebrauch der Zuweisungsregel üben in der Vorlesung: * Erläuterung und Begründung der Beispiele; * Aus der gewünschten Nachbedingung die Vorbedingung herstellen. * Dann zeigen, dass die Vorbedingung wirklich gilt. -------------------------------------------------------------------------------- Mod - 4.59 Schlussregeln für Sequenz Sequenzregel: Bedeutung: {P} S1 {Q} Wenn {P} S1 {Q} und {Q} S2 {R} korrekte Schlüsse sind, {Q} S2 {R} dann ist auch {P} S1; S2 {R} ein korrekter Schluss {P} S1; S2 {R} Beispiel: { x>0 logicaland y>0 } a := x; { a>0 logicaland y>0 } { a>0 logicaland y>0 } b := y; { a>0 logicaland b>0 } { x>0 logicaland y>0 } a := x; b := y;{ a>0 logicaland b>0 } im Algorithmus die Schritte zusammensetzen: { x>0 logicaland y>0 } { x>0 logicaland y>0 } a := x; und a := x; { a>0 logicaland y>0 } { a>0 logicaland y>0 } { a>0 logicaland y>0 } b := y; b := y; { a>0 logicaland b>0 } { a>0 logicaland b>0 } (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 459 Ziele: Sequenzregel anwenden können in der Vorlesung: * Prinzip an der Sequenzregel erläutern * Beispiel erläutern -------------------------------------------------------------------------------- Mod - 4.60 Konsequenzregeln Abschwächung der Nachbedingung Verschärfung der Vorbedingung { P } S { R } { P } arrowright { R } { R } arrowright { Q } { R } S { Q } { P } S { Q } { P } S { Q } Beispiel: im Algorithmus können Implikationen in Ausführungsrichtung eingefügt werden: { a+b > 0 } x := a+b { x > 0 } { a+b > 0 } { x > 0 } arrowright { x greaterequal 0} x := a+b { x > 0 } arrowright { 2*x greaterequal 0} { a+b > 0 } x := a+b { x greaterequal 0 } y := 2*x { y greaterequal 0} (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 460 Ziele: Vor- und Nachbedingung anpassen in der Vorlesung: * Anwendung beim Zusammensetzen von Algorithmenschritten zeigen Verständnisfragen: -------------------------------------------------------------------------------- Mod - 4.61 Regel für 2-seitige Alternative { P logicaland B } S1 { Q } Aus der { P logicaland logicalnot B } S2 { Q } gemeinsamen Vorbedingung P führen beide Zweige auf { P } falls B: S1 sonst S2 { Q } dieselbe Nachbedingung Q Beispiel: im Algorithmus: { true logicaland a > 0 } b := a { b > 0 } arrowright { b greaterequal 0 } { a>0 logicaland b>0 logicaland a notequal b } { true logicaland logicalnot (a > 0) } arrowright { -a greaterequal 0 } b := - a { b greaterequal 0 } falls a > b : { a>0 logicaland b>0 logicaland a>b } arrowright { true } falls a > 0: b := a sonst b := - a { b greaterequal 0 } { a-b>0 logicaland b>0 } a := a - b { a>0 logicaland b>0 } sonst { a>0 logicaland b>0 logicaland b>a } arrowright { a>0 logicaland b-a>0 } b := b - a { a>0 logicaland b>0 } { a>0 logicaland b>0 } (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 461 Ziele: Regel verstehen in der Vorlesung: * Beide Zweige müssen auf dieselbe Aussage führen * Beispiele zeigen * Konsequenzregeln mitverwenden -------------------------------------------------------------------------------- Mod - 4.62 Regel für bedingte Anweisung Aus der { P logicaland B } S { Q } P logicaland logicalnot B arrowright Q gemeinsamen Vorbedingung P führen die Anweisung und die Implikation auf dieselbe Nachbedingung Q { P } falls B : S { Q } Beispiel: im Algorithmus: { P logicaland a < 0 } arrowright { -a greaterequal 0 } a := - a { a greaterequal 0 } { P } falls a < 0 : P logicaland logicalnot (a < 0) arrowright a greaterequal 0 { P logicaland a < 0 } arrowright { -a greaterequal 0 } a := - a; { P } falls a < 0: a := -a { a greaterequal 0 } { a greaterequal 0 } leere Alternative: { P logicaland logicalnot (a < 0)} arrowright { a greaterequal 0 } { a greaterequal 0 } (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 462 Ziele: Regel verstehen in der Vorlesung: * Die leere Alternative muss auf dieselbe Aussage führen wie die Anweisung. * leere Alternative im Algorithmus sichtbar machen. * Beispiele zeigen. -------------------------------------------------------------------------------- Mod-4.63 Aufrufregel Der Unteralgorithmus UA habe keine Parameter und liefere kein Ergebnis. Seine Wirkung auf globale Variable sei spezifiziert durch die Vorbedingung P und die Nachbedingung Q. Dann gilt für einen Aufruf von UA die Schlussregel { P } UA() { Q } (Ohne Parameter und Ergebnis ist diese Regel nur von sehr begrenztem Nutzen.) (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 463 Ziele: Einfache Aufrufregel in der Vorlesung: Erläuterungen und Beispiel dazu -------------------------------------------------------------------------------- Mod - 4.64 Schleifenregel Wiederholung, Schleife: { INV logicaland B } S { INV } { INV } solange B wiederhole S { INV logicaland logicalnot B } Eine Aussage P heißt Schleifeninvariante, wenn man zeigen kann, dass sie an folgenden Stellen gilt: vor der Schleife, vor und nach jeder Ausführung von S und nach der Schleife. Beispiel: Algorithmus zum Potenzieren a := x; b := y; z := 1; INV: z dotmath ab = xy { INV } logicaland b greaterequal 0 solange b > 0 wiederhole { INV logicaland b > 0 } arrowboth { z dotmath a dotmath ab-1 = xy logicaland (b-1) greaterequal 0 } b := b - 1; { z dotmath a dotmath ab = xy logicaland b greaterequal 0 } z := z dotmath a { INV } { INV logicaland b lessequal 0 } arrowboth { z dotmath ab = xy logicaland b = 0 } arrowright { z = xy } (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 464 Ziele: Schleifeninvariante verstehen in der Vorlesung: Erläuterungen dazu * Das Prinzip Invariante erläutern. * Schlussregel erläutern. * Am Beispiel mehrere Invariante zeigen. -------------------------------------------------------------------------------- Mod-4.65 Terminierung von Schleifen Die Terminierung einer Schleife solange B wiederhole S muss separat nachgewiesen werden: 1. Gib einen ganzzahligen Ausdruck E an über Variablen, die in der Schleife vorkommen, und zeige, dass E bei jeder Iteration durch S verkleinert wird. 2. Zeige, dass E nach unten begrenzt ist, z. B. dass 0 lessequal E eine Invariante der Schleife ist. Es kann auch eine andere Grenze als 0 gewählt werden. E kann auch monoton vergrößert werden und nach oben begrenzt sein. Nichtterminierung wird bewiesen, indem man zeigt, dass R logicaland B eine Invariante der Schleife ist und dass es eine Eingabe gibt, so dass R logicaland B vor der Schleife gilt. R kann einen speziellen Zustand charakterisieren, in dem die Schleife nicht anhält. Es gibt Schleifen, für die man nicht entscheiden kann, ob sie für jede Vorbedingung terminieren. (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 465 Ziele: Terminierungsnachweis verstehen in der Vorlesung: * Erläuterungen zu den Schritten. * Der Ausdruck E braucht selbst nicht in der Schleife vorzukommen. * Beispiele dazu. -------------------------------------------------------------------------------- Mod-4.66 Beispiele zur Terminierung (1) { a > 0 logicaland b > 0} 1. Schleife1 solange a notequal b wiederhole Schleife2 solange a > b wiederhole a := a - b; Schleife3 solange a < b wiederhole b := b - a terminiert weil: a. INV = a > 0 logicaland b > 0 ist Invariante für jede der 3 Schleifen, denn {INV} Schleife1 solange a notequal b wiederhole {INV logicaland a notequal b} Schleife2 solange a > b wiederhole {INV logicaland a > b}arrowright {a-b > 0 logicaland b > 0} a := a - b; {INV} {INV} Schleife3 solange a < b wiederhole {INV logicaland a < b}arrowright {a > 0 logicaland b-a > 0} b := b - a {INV} {INV} {INV} b. Schleife2: a fällt monoton, weil b > 0; a ist begrenzt, weil a > 0. Schleife3: b fällt monoton, weil a > 0; b ist begrenzt, weil b > 0. Schleife1: a+b fällt monoton, weil wg. a notequal b Schl. 2 o. 3 mind. 1x iteriert wird; a+b begrenzt, wg. INV. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 466 Ziele: Terminierungsnachweis üben in der Vorlesung: * 1 und 2 durch geeignete Invariante begründen * 3 wird nicht versucht, zu entscheiden -------------------------------------------------------------------------------- Mod-4.66a Beispiele zur Terminierung (2) 2. { a > 0 logicaland b > 0} Schleife1 solange a notequal b wiederhole Schleife2 solange a greaterequal b wiederhole a := a - b; Schleife3 solange a < b wiederhole b := b - a terminiert nicht immer: a > 0 ist nicht invariant in den Schleifen. Die Nachbedingung von Schleife 2 ist a < b logicaland a greaterequal 0. Schleife 3 kann erreicht werden im Zustand R: a = 0, z.B. wenn initial a = 2*b gilt. a = 0 logicaland a < b ist invariant in Schleife 3 und a < b ist die Schleifenbedingung. {a = 0 logicaland a < b} arrowright {a = 0 logicaland a < b-a} b := b - a {a = 0 logicaland a < b} (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 466a Ziele: Terminierungsnachweis üben in der Vorlesung: * 1 und 2 durch geeignete Invariante begründen * 3 wird nicht versucht, zu entscheiden -------------------------------------------------------------------------------- Mod-4.66b Beispiele zur Terminierung (3) 3. { n element Iota N logicaland n > 1 } solange n > 1 wiederhole falls n gerade: n := n / 2 sonst n := 3 * n + 1 Terminierung / Nichtterminierung ist unbewiesen; einige Ausführungen mit Anfangswerten n: n 2 1 3 10 5 16 8 4 2 1 4 2 1 5 16 8 4 2 1 6 3 10 5 16 8 4 2 1 7 22 11 34 17 52 26 13 50 25 76 38 19 ... (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 466b Ziele: Terminierungsnachweis üben in der Vorlesung: * 1 und 2 durch geeignete Invariante begründen * 3 wird nicht versucht, zu entscheiden -------------------------------------------------------------------------------- Mod-4.67 Denksportaufgabe zu Invarianten In einem Topf seien s schwarze und w weiße Kugeln, s + w > 0 solange mindestens 2 Kugeln im Topf sind nimm 2 beliebige Kugeln heraus falls sie gleiche Farbe haben: wirf beide weg und lege eine neue schwarze Kugel in den Topf falls sie verschiedene Farben haben: lege die weiße Kugel zurück in den Topf und wirf die schwarze Kugel weg Welche Farbe hat die letzte Kugel? Finden Sie Invarianten, die die Frage beantworten. (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 467 Ziele: Passende Invarianten finden in der Vorlesung: * Lösung erfragen. -------------------------------------------------------------------------------- Mod-4.68 Schrittweise Konstruktion und Verifikation Vorbedingung: x element Iota R und n element Iota N0 Konstruktionsidee: Nachbedingung: q = xn Invariante INV: xn = q * ai logicaland i greaterequal 0 Algorithmus: Zielbedingung: i lessequal 0 { n greaterequal 0 } arrowright { n = n logicaland n greaterequal 0 logicaland x = x logicaland 1 = 1 } falls i gerade: xn = q * (a2)i/2 a := x; q := 1; i := n; falls i ungerade: xn = q * a * (a2)i/2 { i = n logicaland i greaterequal 0 logicaland a = x logicaland q = 1 } arrowright { INV } solange i > 0 wiederhole { INV logicaland i > 0 } falls i ungerade: { INV logicaland i > 0 logicaland i ungerade } arrowright { xn = q * a * (a2)i/2 logicaland i > 0 } q := q * a; { xn = q * (a2)i/2 logicaland i > 0 } leere Alternative für i gerade: { INV logicaland i > 0 logicaland i gerade } arrowright { xn = q * (a2)i/2 logicaland i > 0 } Schritte: 1. Vor-, Nachbedingung { xn = q * (a2)i/2 logicaland i > 0 } 2. Schleifeninvariante a := a * a; { xn = q * ai/2 logicaland i > 0 } arrowright { xn = q * ai/2 3. Schleife mit INV logicaland i/2 greaterequal 0 } 4. Initialisierung i := i / 2 5. Idee für Schleifenrumpf { xn = q * ai logicaland i greaterequal 0 } arrowboth { INV } 6. Alternative { INV logicaland i lessequal 0 } arrowright { q = xn } 7. Schleife komplett 8. Terminierung Terminierung der Schleife: i fällt monoton und i greaterequal 0 ist invariant. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 468 Ziele: Entwicklung eines vollständigen Beispiels in der Vorlesung: Erläuterung der einzelnen Schritte. In der Datei verifikation.pdf findet man die schrittweise Entwicklung des Inhaltes der Folie. --------------------------------------------------------------------------------