Institut für Parallele und Verteilte Systeme Universität Stuttgart Universitätsstraße 38 D–70569 Stuttgart Bachelorarbeit Invarianten von Ansatzfunktionen beim Basiswechsel Kamigar Mohamadsharief Studiengang: Informatik Prüfer/in: Prof. Dr. rer. nat. Miriam Schulte Betreuer/in: Dr. Stefan Zimmer Beginn am: 8. Dezember 2021 Beendet am: 8. Juni 2022 Kurzfassung Diese Bachelorarbeit beschäftigt sich mit der formalen Verifikation des newtonschen Ansatzes für die Interpolation. Hierfür wird ein Basiswechsel hergeleitet und bewiesen, dass die Transformationen der Basis die korrekten Ansatzfunktionen berechnen, wodurch die Verifikation des gesamten Algorithmus folgt. Es wird auch erörtert inwiefern sich Herangehensweisen für den Beweis und Umformungen des Algorithmus auf andere Algorithmen in der Numerik übertragen lassen. 3 Inhaltsverzeichnis 1 Einleitung 7 2 Grundlagen 9 3 Herleitung des Basiswechsels 13 4 Konstruktion der Schleifeninvarianten 21 4.1 Invariante der äußeren WHILE-Schleife . . . . . . . . . . . . . . . . . . . . . 21 4.2 Invariante der inneren WHILE-Schleife . . . . . . . . . . . . . . . . . . . . . . 24 5 Verifikation des Algorithmus 29 5.1 Korrektheitsbeweis der äußeren WHILE-Schleife . . . . . . . . . . . . . . . . . 29 5.2 Korrektheitsbeweis der inneren WHILE-Schleife . . . . . . . . . . . . . . . . . 33 6 Diskussion und Ausblick 43 Literaturverzeichnis 45 5 1 Einleitung Wenn herausgefunden werden soll, ob ein Programm eine gewünschte Funktionalität erfüllt, wird üblicherweise das Programm auf verschiedene Eingaben überprüft. Diese Herangehensweise zeigt jedoch nur wie das Programm auf die vordefinierten Eingaben reagiert, aber beweist nicht dessen Korrektheit. Somit kann der Programmierer nur überzeugt sein, dass das Programm korrekt abläuft, was das Programm nicht unbedingt fehlerfrei macht und keinem formalen Beweis gleicht. Um die Korrektheit eines Programms zu beweisen eignet sich die Anwendung des Hoare-Kalküls, welches mithilfe von mathematischer Logik ein formales System beschreibt. Im Hoare-Kalkül werden für ein auszuführendes Programmsegment jeweils ein Prädikat für die Vorbedingung definiert, welches vor der Ausführung des Programmsegmentes gilt und ein Prädikat für die Nachbedingung, welches nach der Ausführung gilt. Die formale Korrektheit des Programmsegmentes ist gegeben wenn bei geltender Vorbedingung das Programmsegment ausgeführt wird und anschließend die Nachbedingung gilt. Im Allgemeinen wird für die Vorbedingung der initiale Zustand vor Ausführung des Programmsegments gewählt und die gewünschte Funktionalität beschreibt die Nachbedingung. Diese Herangehensweise wird für jede Anweisung im Programm angewandt, mit dem Ziel, dass das Programm als Ganzes formal verifiziert wird. Kommt in einem Programm eine Schleife vor, wird für die Verifikation der Schleife neben einer Vor- und Nachbedingung ein weiteres Prädikat benötigt, welches in der Schleife invariant ist. Invarianz bedeutet hier, dass das Prädikat sowohl vor- und nach der Schleife gilt als auch vor- und nach jedem Schleifendurchlauf. In LAFF-On Programming for Correctness [MG20] präsentieren M. E. Myers und R. A. van de Geijn das Hoare-Kalkül im Detail und erläutern die theoretischen Grundlagen, welche benötigt werden für die Beweisführung in der Verifikation von Programmsegmenten. Außerdem legen sie dar, wie durch gegebene Vor- und Nachbedingungen systematisch Hypothesen für Invarianten von Schleifen konstruiert werden können und darüber hinaus, wie die Anweisungen in der Schleife hergeleitet werden können. In der Forschung wird das Hoare-Kalkül beispielsweise in eingebetteten Softwaresystemen für die Verifikation angewandt von L. Zou et al. [ZZW+13] Das Werkzeug KeY [BH16] von R. Bubel und R. Hähnle ermöglicht eine automatische formale Verifikation von Algorithmen in Java, wobei nur die Eingabe von Schleifeninvarianten ein nichttrivialen Teil der Verifikation darstellt. W. Gander[Gan05] stellt verschiedene Ansätze für die Polynominterpolation vor und un- tersucht die Basiswechsel zwischen den Ansatzfunktionen, welche durch unter anderem in der Lagrange-Basis und in der Newton-Basis repräsentiert werden. Die Bachelorarbeit vom Philip Urban [Urb21] beschäftigt sich mit der Verifikation von drei Algorithmen aus der Numerik. Unter anderem verifiziert er die Korrektheit der dividierten Differenzen, welche die führenden Koeffizienten der Basisfunktionen des newtonschen Algorithmus für die Interpolation sind. In dieser Bachelorarbeit wird mithilfe des Hoare-Kalküls die formale Verifikation der Ansatzfunk- tionen des newtonschen Algorithmus für die Interpolation durchgeführt. Diese Ansatzfunktionen werden während der Berechnung der dividierten Differenzen durch einen Basiswechsel von der Lagrange-Basis in die Newton-Basis hinübergeführt. Um diesen Beweis durchführen zu können, werden im zweiten Kapitel die grundlegenden Regeln des Hoare-Kalküls erklärt. Daraufhin wird 7 1 Einleitung durch Umformungen der Algorithmus verändert, sodass neben der Berechnung der dividierten Differenzen, die Ansatzfunktionen durch einen Wechsel in der Basis berechnet werden. Hierbei ist wichtig zu wissen, dass diese Umformungen das interpolierte Polynom nicht ändern zur Laufzeit des Algorithmus. Dadurch kann gezeigt werden, dass die Verifikation der Ansatzfunktionen in diesem Fall auch die Korrektheit der dividierten Differenzen impliziert. In Kapitel 4 werden Hypothesen für Schleifeninvarianten formuliert, welche systematisch hergeleitet werden können. Darauf aufbauend, wird dann die formale Verifikation durchgeführt. Zum Schluss findet noch eine Diskussion und ein Ausblick statt. 8 2 Grundlagen Hoare-Tripel Dieses Kapitel basiert auf den Grundlagen des Hoare-Kalküls wie sie in LAFF-On Pro- gramming for Correctness [MG20] vorgestellt sind. Mithilfe des Hoare-Kalküls lässt sich formal die Korrektheit von Programmen beweisen. Für einzelne Programmsegmente wird die Notation des Hoare-Tripel verwendet, wobei ein Hoare-Tripel aus den Prädikaten 𝑄, welches die Vorbedingung des Programmsegments 𝑆 beschreibt und 𝑅 für die Nachbedingung. Das Hoare-Tripel {𝑄} 𝑆 {𝑅} evaluiert zu 𝑇𝑅𝑈𝐸 , wenn das Programmsegment 𝑆 in einem Zustand ausgeführt wird, in welchem 𝑄 gilt, und nach der Ausführung im resultierenden Zustand 𝑅 gilt. Außerdem muss die Ausführung von 𝑆 in einer endlichen Zeit erfolgen. In dieser Arbeit werden nur Programmsegmente untersucht, welche mathematische Zuweisungen sind, daher wird die Terminierung hier angenommen. Gibt es keine Vorbedingung wird𝑇𝑅𝑈𝐸 als Vorbedingung gewählt. Aus Platz- und Lesbarkeitsgründen wird {𝑄}𝑆{𝑅} verwendet. Komposition Bei einer Komposition von Anweisungen 𝑆1; 𝑆2 lassen sich die zugehörigen Hoare-Tripel der Form {𝑄}𝑆1{𝑃} ∧ {𝑃}𝑆2{𝑅} ⇒ {𝑄}𝑆1; 𝑆2{𝑅} zu einem Hoare-Tripel zusammensetzen. Schwächste Vorbedingung Um die Korrektheit der Hoare-Tripel zu zeigen, benutzt man die Definition der schwächsten Vorbedingung 𝑤𝑝(”𝑆”, 𝑅), welche alle Zustände beschreibt, bei welchen nach der Ausführung von 𝑆 ein Zustand existiert in welchem 𝑅 gilt. Das Hoare-Tripel {𝑄}𝑆{𝑅} evaluiert genau dann zu 𝑇𝑅𝑈𝐸 , wenn 𝑄 ⇒ 𝑤𝑝(”𝑆”, 𝑅). Dies ist der Fall, da um das Hoare-Tripel zu validieren muss ein Zustand, welcher von der 9 2 Grundlagen schwächsten Vorbedingung beschrieben wird vorliegen. Also muss 𝑄 Zustände beschreiben, welche durch 𝑤𝑝(”𝑆”, 𝑅) gedeckt werden, da sonst das Hoare-Tripel nicht validiert. Schwächste Vorbedingung für Zuweisungen Die Berechnung der schwächsten Vorbedingung für Zuweisungen findet wie folgt statt: für 𝑆 : 𝑥 := 𝐸 wobei 𝐸 ein mathematischer Ausdruck ist 𝑤𝑝(”𝑥 := 𝐸”, 𝑅) = 𝑅𝑥 (𝐸) Das Prädikat 𝑅𝑥 (𝐸) beschreibt das Prädikat 𝑅, bei welchem alle freien Vorkommnisse von 𝑥 durch den Ausdruck (𝐸) ersetzt werden. Diese Regel wird im weiteren Verlauf dieser Arbeit die Zuweisungsregel genannt. Schwächste Vorbedingung für Kompositionen von Zuweisungen Die schwächste Vorbedingung von Hoare-Tripeln mit 𝑛 Anweisungen wird durch 𝑤𝑝(”𝑆1; 𝑆2; ...; 𝑆𝑛”, 𝑅) = 𝑤𝑝(”𝑆1”, 𝑤𝑝(”𝑆2; ...; 𝑆𝑛”, 𝑅)) = 𝑤𝑝(”𝑆1”, 𝑤𝑝(”𝑆2”, 𝑤𝑝(..., 𝑤𝑝(”𝑆𝑛”, 𝑅)))) Diese Regel wird im weiteren Verlauf dieser Arbeit die Kompositionsregel für schwächste Vorbedingungen genannt. WHILE Theorem Das WHILE Theorem zeigt, wie die partielle Korrektheit von WHILE-Schleifen der Form: while 𝐺 do 𝑆 end while bewiesen werden kann, wobei 𝑆 = 𝑆1; ...; 𝑆𝑛 aus 𝑛 Anweisungen zusammengesetzt ist und 𝐺 hier die Schleifenbedingung definiert. 10 Zunächst wird die WHILE-Schleife mit Prädikaten annotiert: {𝑄} {𝐼𝑁𝑉} while 𝐺 do {𝐼𝑁𝑉 ∧ 𝐺} 𝑆 {𝐼𝑁𝑉} end while {𝐼𝑁𝑉 ∧ ¬𝐺} {𝑅} • 𝐼𝑁𝑉 ist hier die Schleifeninvariante, welche vor dem ersten Schleifendurchlauf gilt, weshalb 𝑄 ⇒ 𝐼𝑁𝑉 gelten muss. • Beim erstmaligem Betreten der WHILE-Schleife gilt die Schleifeninvariante 𝐼𝑁𝑉 , da keine Anweisungen ausgeführt wurden und nur die Schleifenbedingung 𝐺 überprüft wurde und auch gilt. • Wenn {𝐼𝑁𝑉 ∧ 𝐺}𝑆{𝐼𝑁𝑉} gilt, dann gilt 𝐼𝑁𝑉 auch am Ende eines Schleifendurchlaufs und am Anfang des nächsten Schleifendurchlaufs. • Wird die WHILE-Schleife verlassen so gilt 𝐼𝑁𝑉 immer noch und ¬𝐺, da am Ende des letzten Schleifendurchlaufs 𝐼𝑁𝑉 galt und beim Verlassen der WHILE-Schleife keine Anweisungen ausgeführt wurden. • Wenn schließlich 𝐼𝑁𝑉 ∧ ¬𝐺 ⇒ 𝑅 gilt ist die Korrektheit der WHILE-Schleife im Bezug zur Nachbedingung 𝑅 bewiesen. Für WHILE-Schleifen der obigen Form muss daher für die partielle Korrektheit folgendes bewiesen werden: 1. 𝑄 ⇒ 𝐼𝑁𝑉 2. {𝐼𝑁𝑉 ∧ 𝐺}𝑆{𝐼𝑁𝑉} 3. 𝐼𝑁𝑉 ∧ ¬𝐺 ⇒ 𝑅 Für die vollständige Korrektheit neben der partiellen Korrektheit noch die Terminierung der WHILE-Schleife bewiesen werden. Beim Gebrauch des WHILE-Theorems werden hier ausschließlich WHILE-Schleifen behandelt, welche umgeformte FOR-Schleifen sind, die von einem endlichen Eingabeparameter abhängen. Daher wird die Terminierung hier angenommen und für die vollständige Korrektheit genügt es hier die partielle Korrektheit zu beweisen. {𝑄}while(𝐺)𝑆endwhile{𝑅} ist die Kurzschreibweise für ein Hoare-Tripel mit einer WHILE- Schleife als Programmsegment. 11 3 Herleitung des Basiswechsels Im vorangegangenen Kapitel wurden die Grundlagen für das Hoare-Kalkül näher erläutert. Nun soll der newtonsche Algorithmus für die Interpolation so modifiziert werden, dass neben der Berechnung der Koeffizienten der Polynome in der Newton-Basis, auch die Polynome der Lagrange-Basis durch Transformationen in die Newton-Basis umgeformt werden. Dabei ist zu beachten, dass am Anfang des Algorithmus das zu interpolierende Polynom durch die Lagrange-Basis dargestellt wird. Außerdem soll sich bei der Berechnung der dividierten Differenzen und der Ansatzfunktionen in der Newton-Basis das zu interpolierende Polynom nicht verändern. Diese Eigenschaft wird in diesem Kapitel erneut aufgegriffen und ist maßgebend für die Verifikation des Algorithmus. Dividierte Differenzen Der newtonsche Algorithmus für die Interpolation in 3.1 erhält als Eingabe die paarwei- se verschiedenen Stützpunkte der zu interpolierenden Funktion und berechnet die führenden Koeffizienten [𝑥𝑖 , ..., 𝑥𝑛] 𝑓 der Polynome in der Newton-Basis. Diese Koeffizienten werden im newtonschen Ansatz dividierte Differenzen genannt. Eingabe: 𝑛 + 1 Stützpunkte (𝑥𝑖 , 𝑓 (𝑥𝑖)) , 0 ≤ 𝑖 ≤ 𝑛 Algorithmus 3.1 Newtonsches Interpolationsverfahren 1: for 𝑖 = 0, ..., 𝑛 do 2: 𝑑𝑖 := 𝑓 (𝑥𝑖); 3: end for 4: for 𝑘 = 1, ..., 𝑛 do 5: for 𝑖 = 𝑛, ..., 𝑘 do 6: 𝑑𝑖 := (𝑑𝑖 − 𝑑𝑖−1)/(𝑥𝑖 − 𝑥𝑖−𝑘); 7: end for 8: end for 9: return[𝑥0] 𝑓 = 𝑑0, ..., [𝑥0, ..., 𝑥𝑛] 𝑓 = 𝑑𝑛 13 3 Herleitung des Basiswechsels Das zu interpolierende Polynom ergibt sich aus: 𝑃(𝑥) = 𝑛∑︁ 𝑖=0 ( 𝑑𝑖 · 𝜋𝑖 (𝑥) ) mit 𝜋𝑖 (𝑥) = 𝑖−1∏ 𝑘=0 (𝑥 − 𝑥𝑘) und 𝜋(𝑥) = ( 𝜋0(𝑥) ... 𝜋𝑛 (𝑥) )⊤ wobei hier 𝜋(𝑥) die Newton-Basis darstellt Die Polynome in der Newton-Basis werden im modifizierten Algorithmus aus den Poly- nomen in der Lagrange-Basis berechnet, welche wie folgt definiert sind: 𝑙𝑖 (𝑥) = 𝑛∏ 𝑘=0 𝑘≠𝑖 𝑥 − 𝑥𝑘 𝑥𝑖 − 𝑥𝑘 mit 𝑃(𝑥) = 𝑛∑︁ 𝑖=0 𝑓𝑖 · 𝑙𝑖 (𝑥) 𝑙 (𝑥) = ( 𝑙0(𝑥) ... 𝑙𝑛 (𝑥) )⊤ außerdem wird 𝑙 (𝑥) die Lagrange-Basis genannt. Initalisierung Die dividierten Differenzen sind bei der Initialisierung bereits gleich den Funktionswer- ten an den Stützstellen, weshalb zur Initialisierung die Ansatzfunktionen in der Lagrange-Basis repräsentiert werden können. 𝜑𝑖 sind die Ansatzfunktionen, welche bei der Initialisierung der Lagrange-Basis gleichen. Die Initialisierung des newtonschen Algorithmus beim Basiswechsel: for 𝑖 = 0, ..., 𝑛 do 𝑑𝑖 := 𝑓 (𝑥𝑖); 𝜑𝑖 (𝑥) := 𝑙𝑖 (𝑥); end for Dann gilt: 𝑃(𝑥) = 𝑛∑︁ 𝑖=0 𝑑𝑖 · 𝜑𝑖 (𝑥) = 𝑛∑︁ 𝑖=0 𝑓 (𝑥𝑖) · 𝑙𝑖 (𝑥) 14 Schleifenkörper Im Endzustand gilt ∀𝑖 ∈ [0, 𝑛] : (𝑑𝑖 = [𝑥𝑖 , ..., 𝑥𝑛] 𝑓 ∧ 𝜑𝑖 (𝑥) = 𝜋𝑖 (𝑥)) ⇒ 𝑃(𝑥) = 𝑛∑︁ 𝑖=0 𝑑𝑖 · 𝜑𝑖 (𝑥) = 𝑛∑︁ 𝑖=0 [𝑥𝑖 , ..., 𝑥𝑛] 𝑓 · 𝜋𝑖 (𝑥) Dies soll auch während jedem Schleifendurchlauf der inneren FOR-Schleife gelten, weil dadurch im gesamten Algorithmus hinweg das Polynom erhalten bleibt. Das hat zur Folge, dass am Ende des Algorithmus das interpolierte Polynom vorliegt und die Polynome der Newton-Basis. Wenn also gezeigt wird, dass am Ende die Polynome der Newton-Basis vorliegen und sich das Polynom während des Algorithmus nicht verändert, müssten die Koeffizienten der Newton-Basis, sprich die dividierten Differenzen korrekt berechnet worden sein, da sonst das zu interpolierende Polynom nicht korrekt dargestellt wird. Für einen Schleifendurchlauf der inneren FOR-Schleife liegt am Anfang der Vektor 𝑑 vor, welcher ein beliebiger sein kann aus R𝑛+1, welcher hier als 𝑑𝑎𝑙𝑡 definiert wird. 𝜑𝑖 (𝑥) wird vor dem Schleifendurchlauf als 𝜑(𝑥)𝑎𝑙𝑡 definiert. Nach dem Schleifendurchlauf liegen 𝑑𝑛𝑒𝑢, 𝜑𝑛𝑒𝑢 vor, an welchen eine Basistransformation durchgeführt wurde. Dann muss gelten: 𝑛∑︁ 𝑎=0 𝑑𝑎𝑙𝑡𝑎 · 𝜑𝑎𝑙𝑡 𝑎 (𝑥) ! = 𝑛∑︁ 𝑎=0 𝑑𝑛𝑒𝑢𝑎 · 𝜑𝑛𝑒𝑢 𝑎 (𝑥) Für 𝑑𝑎𝑙𝑡 werden die Vektoren der kanonischen Basis 𝐵 = {𝑒0, ..., 𝑒𝑛} des Vektorraums R𝑛+1 gewählt mit: 𝑏 ∈ [0, 𝑛] : 𝑑𝑎𝑙𝑡 = 𝑒𝑏 ∀𝑏 ∉ {𝑖 − 1, 𝑖} : 𝑑𝑎𝑙𝑡 = 𝑑𝑛𝑒𝑢 𝑛∑︁ 𝑎=0 𝑑𝑎𝑙𝑡𝑎 · 𝜑𝑎𝑙𝑡 𝑎 (𝑥) = 𝑑𝑎𝑙𝑡𝑏 · 𝜑𝑎𝑙𝑡 𝑏 (𝑥) = 𝜑𝑎𝑙𝑡 𝑏 (𝑥) Mit 𝑑𝑎𝑙𝑡𝑏 = 𝑑𝑛𝑒𝑢𝑏 gilt: 𝜑𝑎𝑙𝑡 𝑏 (𝑥) = 𝜑𝑛𝑒𝑢 𝑏 (𝑥) 15 3 Herleitung des Basiswechsels 𝑏 = 𝑖 − 1 : 𝑑𝑛𝑒𝑢𝑖−1 = 𝑑𝑎𝑙𝑡𝑖−1 = 1 ∧ 𝑑𝑛𝑒𝑢𝑖 = 𝑑𝑎𝑙𝑡 𝑖 − 𝑑𝑎𝑙𝑡 𝑖−1 𝑥𝑖 − 𝑥𝑖−𝑘 = − 1 𝑥𝑖 − 𝑥𝑖−𝑘 ⇒ 𝜑𝑎𝑙𝑡 𝑖−1 = 𝜑𝑛𝑒𝑢 𝑖−1 − 1 𝑥𝑖 − 𝑥𝑖−𝑘 𝜑𝑛𝑒𝑢 𝑖 Auflösen nach 𝜑𝑛𝑒𝑢 𝑖 fliefert: 𝜑𝑛𝑒𝑢 𝑖−1 = 𝜑𝑎𝑙𝑡 𝑖−1 + 1 𝑥𝑖 − 𝑥𝑖−𝑘 𝜑𝑛𝑒𝑢 𝑖 (3.1) 𝑏 = 𝑖 : 𝑑𝑛𝑒𝑢𝑖 = 𝑑𝑎𝑙𝑡 𝑖 − 𝑑𝑎𝑙𝑡 𝑖−1 𝑥𝑖 − 𝑥𝑖−𝑘 = 1 𝑥𝑖 − 𝑥𝑖−𝑘 ⇒ 𝜑𝑎𝑙𝑡 𝑖 = 𝑑𝑎𝑙𝑡 𝑖 − 𝑑𝑎𝑙𝑡 𝑖−1 𝑥𝑖 − 𝑥𝑖−𝑘 𝜑𝑛𝑒𝑢 𝑖 Auflösen nach 𝜑𝑎𝑙𝑡 𝑖−1 liefert: 𝜑𝑛𝑒𝑢 𝑖 = (𝑥𝑖 − 𝑥𝑖−𝑘) · 𝜑𝑎𝑙𝑡 𝑖 (3.2) Durch einsetzen von 3.2 in 3.1 erhält die Gleichung die Form : 𝜑𝑛𝑒𝑢 𝑖−1 = 𝜑𝑎𝑙𝑡 𝑖−1 + 1 𝑥𝑖 − 𝑥𝑖−𝑘 𝜑𝑛𝑒𝑢 𝑖 = 𝜑𝑎𝑙𝑡 𝑖−1 + 1 𝑥𝑖 − 𝑥𝑖−𝑘 (𝑥𝑖 − 𝑥𝑖−𝑘) · 𝜑𝑎𝑙𝑡 𝑖 = 𝜑𝑎𝑙𝑡 𝑖−1 + 𝜑𝑎𝑙𝑡 𝑖 Dadurch ergeben sich die Anweisungen: 𝜑𝑖−1(𝑥) = 𝜑𝑖−1(𝑥) + 𝜑𝑖 (𝑥) 𝜑𝑖 (𝑥) = (𝑥𝑖 − 𝑥𝑖−𝑘) · 𝜑𝑖 (𝑥) welche bei jedem Durchlauf der inneren FOR-Schleife ausgeführt werden. Weil dadurch: 𝑃(𝑥) = 𝑛∑︁ 𝑖=0 𝑑𝑖 · 𝜑𝑖 (𝑥) bei jedem Schleifendurchlauf gilt, muss bewiesen werden, dass Während des Algorithmus auch tatsächlich die Ansatzfunktionen in der Newton-Basis berechnet werden. Das newtonsche Algorithmus für die Interpolation mit einem Basiswechsel von der Lagrange-Basis in die Newton-Basis sieht dann wie folgt aus: 16 Algorithmus 3.2 Newtonscher Algorithmus für die Interpolation mit Basiswechsel 1: for 𝑖 = 0, ..., 𝑛 do 2: 𝑑𝑖 := 𝑓 (𝑥𝑖) 3: 𝜑𝑖 (𝑥) := 𝑙𝑖 (𝑥) 4: end for 5: for 𝑘 = 1, ..., 𝑛 do 6: for 𝑖 = 𝑛, ..., 𝑘 do 7: 𝑑𝑖 := (𝑑𝑖 − 𝑑𝑖−1)/(𝑥𝑖 − 𝑥𝑖−𝑘) 8: 𝜑𝑖−1(𝑥) = 𝜑𝑖−1(𝑥) + 𝜑𝑖 (𝑥) 9: 𝜑𝑖 (𝑥) = (𝑥𝑖 − 𝑥𝑖−𝑘) · 𝜑𝑖 (𝑥) 10: end for 11: end for 12: return 𝑑0, ..., 𝑑𝑛 ∧ 𝜑0, ..., 𝜑𝑛 Matrixschreibweise Um die Anweisungen für den Basiswechsel alternativ herzuleiten, eignet es sich den Al- gorithmus in Matrixschreibweise zu notieren. Dann wird für den Vektor 𝜑(𝑥) = ©­­« 𝜑0(𝑥) 𝜑𝑛 (𝑥) ª®®¬ die Matrix mit der Form 𝜙 = ©­­« 𝜑0(𝑥0) 𝜑0(𝑥𝑛) 𝜑𝑛 (𝑥0) 𝜑𝑛 (𝑥𝑛) ª®®¬ verwendet. Die Funktionswerte an den Stützstellen 𝑓 = ©­­« 𝑓0 𝑓𝑛 ª®®¬ werden durch 𝑓 = 𝜙⊤𝑑 berechnet. Das zu interpolierende Polynom lässt sich mit 𝑃(𝑥) = 𝑑⊤(𝜙 · 𝑙 (𝑥)) = 𝑑⊤𝜋(𝑥) darstellen. 17 3 Herleitung des Basiswechsels Die Anweisung: 7. 𝑑𝑖 = (𝑑𝑖 − 𝑑𝑖−1)/(𝑥𝑖 − 𝑥𝑖−𝑘) wird durch die äquivalente Anweisung: 7. 𝑑 = 𝐴(𝑖, 𝑘) · 𝑑 mit 𝐴(𝑖, 𝑘) = ©­­­­­­­­« 𝑖 − 1 𝑖 1 −1 (𝑥𝑖−𝑥𝑖−𝑘) 1 (𝑥𝑖−𝑥𝑖−𝑘) 𝑖 1 ª®®®®®®®®¬ ersetzt. Um nun herzuleiten, welche Matrix 𝑋 die Matrix 𝜙 transformieren soll, müssen die Funktionswerte der Stützstellen während dem Algorithmus erhalten bleiben, daher: 𝑓 = 𝜙⊤𝑑 = (𝑋𝜙)⊤ · 𝐴(𝑖, 𝑘)𝑑 Diese Gleichung geht für 𝑋 = 𝐴(𝑖, 𝑘)−⊤ auf, da: 𝑓 = (𝐴(𝑖, 𝑘)−⊤𝜙)⊤ · 𝐴(𝑖, 𝑘)𝑑 = 𝜙⊤𝐴(𝑖, 𝑘)−1 · 𝐴(𝑖, 𝑘)𝑑 = 𝜙⊤𝑑 Also wird die Matrix 𝜙 mit 𝐴(𝑖, 𝑘)−⊤ transformiert, welche wie folgt aussieht: 𝐴(𝑖, 𝑘)−⊤ = ©­­­­­­­­­­« 𝑖 − 1 𝑖 1 1 1 𝑖 − 1 0 𝑥𝑖 − 𝑥𝑖−𝑘 𝑖 1 ª®®®®®®®®®®¬ 18 Der resultierende Algorithmus für newtonschen Ansatz für die Interpolation mit einem Basiswechsel muss so modifiziert werden, sodass keine FOR-Schleifen mehr darin vorkommen, da das Hoare- Kalkül nur mit WHILE-Schleifen operieren kann. Die FOR-Schleife für die Initialisierung kann wegfallen und durch Zuweisungen von Vektoren und Matrizen ersetzt werden. Der Vektor für die dividierten Differenzen wird dem Vektor der Funktionswerte der Stützstellen initialisiert. Die Matrix 𝜙 für die Ansatzfunktionen wird mit der Einheitsmatrix in R𝑛+1 initialisiert, wegen: ∀𝑖, 𝑗 ∈ [0, 𝑛] : 𝜙𝑖, 𝑗 = 𝑙𝑖 (𝑥 𝑗) und 𝑙𝑖 (𝑥 𝑗) = { 1 𝑖 = 𝑗 0 sonst Die weiteren FOR-Schleifen werden in WHILE-Schleifen umgeändert. Algorithmus 3.3 Angepasstes newtonsches Interpolationsverfahren mit Basiswechsel in Matrix- schreibweise 1: 𝑘 = 1 2: 𝑖 = 𝑛 3: 𝑑 = 𝑓 4: 𝜙 = 𝐼𝑛+1 5: while 𝑘 ≤ 𝑛 do 6: 𝑖 = 𝑛 7: while 𝑖 ≥ 𝑘 do 8: 𝑑 = 𝐴(𝑖, 𝑘) · 𝑑 9: 𝜙 = 𝐴(𝑖, 𝑘)−⊤ · 𝜙 10: 𝑖 = 𝑖 − 1 11: end while 12: 𝑘 = 𝑘 + 1 13: end while 14: return 𝑑, 𝜙 19 3 Herleitung des Basiswechsels Zum Schluss fehlt noch, den Algorithmus mit Hoare-Tripeln zu annotieren, welche vom WHILE Theorem abgeleitet werden: Algorithmus 3.4 Angepasstes newtonsches Interpolationsverfahren mit Hoare-Tripeln 1: 𝑘 = 1 2: 𝑖 = 𝑛 3: 𝑑 = 𝑓 4: 𝜙 = 𝐼𝑛+1 5: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } 6: while 𝑘 ≤ 𝑛 do 7: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛)} 8: 𝑖 = 𝑛 9: {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 } 10: while 𝑖 ≥ 𝑘 do 11: {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘)} 12: 𝑑 = 𝐴(𝑖, 𝑘) · 𝑑 13: 𝜙 = 𝐴(𝑖, 𝑘)−⊤ · 𝜙 14: 𝑖 = 𝑖 − 1 15: {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 } 16: end while 17: {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ ¬(𝑖 ≥ 𝑘)} 18: 𝑘 = 𝑘 + 1 19: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } 20: end while 21: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ ¬(𝑘 ≤ 𝑛)} 22: return 𝑑, 𝜙 20 4 Konstruktion der Schleifeninvarianten Um systematisch Schleifeninvarianten für WHILE-Schleifen zu bestimmen, ist das Betrachten der Vor und Nachbedingungen wichtig, da sie den Start- und Endzustand darstellen und die Schleifeninvariante unter anderem diese beiden Zustände vor und nach der Schleife decken muss. Weil die Invariante nach jedem Durchlauf der Schleife gilt, muss diese auch den Fortschritt nach jedem Schleifendurchlauf festhalten. Die Schleifeninvariante soll nur so konstruiert sein, dass bei der Verifikation des Algorithmus bewiesen wird, dass die Ansatzfunktionen in der Newton-Basis berechnet werden. Die folgende Herleitung der Schleifeninvarianten ist kein Beweis dafür, dass diese die richtige Invarianten beschreibt. Die Richtigkeit der Invarianten ist erst gegeben, wenn die Schleifen mithilfe der Invarianten unter der Anwendung des WHILE Theorems verifiziert sind. 4.1 Invariante der äußeren WHILE-Schleife Um den den Zustand der Matrix 𝜙 in der Invariante festzuhalten, wird ein Prädikat benötigt, welches abhängig von der Schleifenvariable 𝑘 diesen Zustand beschreibt. Das Prädikat wird 𝑃(𝑘) genannt. Wobei 𝑘 auf den Umfang der Schleifenvariable beschränkt wird, mit (𝑘 ≤ 𝑛 + 1). Dass die Beschränkung des Umfangs der zulässigen Werte für die Prädikate nötig ist, wird im nächsten Kapitel beim Beweis des Algorithmus gezeigt. 𝑃(𝑘) muss daher zum Zeitpunkt 𝑘 den Zustand der einzelnen Zeilen der Matrix festhal- ten. Es ist sinnvoll 𝑃(𝑘) in Bereiche der Matrix 𝜙 aufzuteilen. Die Zeilen, welche bereits dem Endzustand entsprechen und daher nicht mehr vom Algorithmus modifiziert werden, werden mit dem Prädikat 𝐹𝐼𝑁 (𝑘) beschrieben. Die Zeilen, welche nicht dem Endzustand entsprechen und daher vom Algorithmus noch modifiziert werden, werden mit dem Prädikat 𝐼𝑁𝑇𝐸𝑅(𝑘) beschrieben. Daraus lässt sich folgern, dass 𝑃(𝑘) sich aus 𝑃(𝑘) ≡ 𝐹𝐼𝑁 (𝑘) ∧ 𝐼𝑁𝑇𝐸𝑅(𝑘) zusammensetzt. 21 4 Konstruktion der Schleifeninvarianten Um die Prädikate 𝐹𝐼𝑁 (𝑘), 𝐼𝑁𝑇𝐸𝑅(𝑘) zu bestimmen können die Vor- und Nachbedingungen aufschlussreich sein, welche gegeben sind mit: Vorbedingung der äußeren Schleife: (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ), (𝜙 = 𝐼𝑛+1) ≡ (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(1) (4.1) Nachbedingung der äußeren Schleife: 𝑃(𝑛 + 1) ≡ ∀𝑖, 𝑗 ∈ [0, 𝑛] : 𝜙𝑖, 𝑗 = 𝑖−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) (4.2) Durch das Betrachten des Algorithmus kann man sehen, dass zum Zeitpunkt 𝑘 die Zeilen im Intervall von [0, 𝑘 − 1) nicht mehr modifiziert werden. Das bedeutet, dass diese Zeilen bereits den gewünschten Zustand der Nachbedingung erreicht haben müssen. Somit lässt sich das Intervall in der Nachbedingung aufteilen in zwei Teile: [ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)ª®¬ ∧ ©­«𝑖′ ∈ [𝑘 − 1, 𝑛] ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ª®¬ ] ∧ (𝑘 ≤ 𝑛 + 1) Wobei der erste Teil, Teil der Invariante ist. Vorläufig kann festgehalten werden, dass 𝐹𝐼𝑁 (𝑘) mindestens die Zeilen [0, 𝑘 − 1) abdeckt mit: 𝐹𝐼𝑁 (𝑘) ≡ ∀𝑖 ′ , 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ª®¬  ∧ (𝑘 ≤ 𝑛 + 1) Für diesen Algorithmus ist die Vorbedingung nicht sehr aufschlussreich, da die Matrix 𝜙 schon beim ersten Schleifendurchlauf alle Zeilen der Matrix modifiziert. Die einzige Information, welche die Vorbedingung für das Konstruieren der Invariante liefert, ist die Eigenschaft, dass zu beginn der Schleife 𝑃(1) gelten muss. Es fehlt noch die Zeilen der Matrix 𝜙 im Intervall [𝑘 − 1, 𝑛] in die Invariante zu integrieren. Um diese in einer Invariante während jedem Schleifendurchlauf zu beschreiben ist es hilfreich die Entwicklung der Matrix 𝜙 an einem allgemeinem Beispiel zu analysieren. 22 4.1 Invariante der äußeren WHILE-Schleife Beispiel Stützstellen 𝑥0, ..., 𝑥3 mit 𝑓 = ©­­« 𝑓0 𝑓3 ª®®¬ Zustand der Matrix 𝜙 für 𝑘 = 2 𝜙 = ©­­­­« 1 1 1 1 0 𝑥1 − 𝑥0 𝑥1 − 𝑥0 𝑥1 − 𝑥0 0 0 𝑥2 − 𝑥1 𝑥2 − 𝑥1 0 0 0 𝑥3 − 𝑥2 ª®®®®¬ und 𝑘 = 3 𝜙 = ©­­­­« 1 1 1 1 0 𝑥1 − 𝑥0 𝑥2 − 𝑥0 𝑥3 − 𝑥0 0 0 (𝑥2 − 𝑥1) (𝑥2 − 𝑥0) (𝑥3 − 𝑥1) (𝑥2 − 𝑥0) 0 0 0 (𝑥3 − 𝑥2) (𝑥3 − 𝑥1) ª®®®®¬ An diesem Beispiel lässt sich Erkennen, dass die Einträge der unteren Dreiecksmatrix also für 𝑗 < 𝑖 ′ immer 0 sind. Begründen lässt sich dies durch die Nachbedingung, welche fordert, dass 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑). Weil für die untere Dreiecksmatrix 𝑗 < 𝑖 ′ gilt, kommt ein Nullprodukt im Produkt vor. Die Einträge weichen auch während des Algorithmus nicht von 0 ab, weil eine Operation auf der Matrix nur eine Multiplikation ist und die andere Operation addiert zwei aufeinanderfolgende Zeilen, wobei 𝑗 < 𝑖 ′ gilt und daher auch 𝑗 < 𝑖 ′ + 1. Aufgrund dieser Observation, lässt sich die untere Dreiecksmatrix in den Endzustand ein- gliedern, weil dessen Einträge sich in der Matrix während der Schleifendurchläufe nicht ändern. 𝐹𝐼𝑁 (𝑘) lässt sich somit wie folgt definieren: 𝐹𝐼𝑁 (𝑘) ≡ ∀𝑖 ′ , 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ª®¬  23 4 Konstruktion der Schleifeninvarianten Aus dem Beispiel wird ersichtlich, bei dem Schleifendurchlauf die Zeile 1 zum letzten mal durch Operationen geändert wird und daher den Endzustand erreicht. Zeile 2 und 3 werden beim nächsten Schleifendurchlauf noch geändert und stellen hier den Zustand der Zeilen dar, welche noch nicht dem Endzustand entsprechen und daher noch geändert werden. Beim genaueren Betrachten fällt auf, dass die einzelnen Terme dem Produkt 𝜋𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) in absteigender Reihenfolge im Bezug auf den Index der Zeile 𝑖 ′, mit jedem Schleifendurchlauf hinzugefügt werden, wobei noch (𝑥𝑖−𝑥𝑖−𝑘) durch die Anweisung 𝜙 = 𝐴(𝑖, 𝑘)−⊤ ·𝜙multipliziert wird. Daher wird 𝐼𝑁𝑇𝐸𝑅(𝑘) wie folgt beschreiben: 𝐼𝑁𝑇𝐸𝑅(𝑘) ≡ [ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑖 ′ ∈ [𝑘 − 1, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧ (𝑘 ≤ 𝑛 + 1) Weil bei der Initialisierung der Teiler zu 0 wird für die Einträge in der Matrix entlang der Diagonale, muss entlang dieser das Intervall aufgeteilt werden. Damit lässt sich 𝐼𝑁𝑇𝐸𝑅(𝑘) darstellen mit: 𝐼𝑁𝑇𝐸𝑅(𝑘) ≡ [ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑖 ′ ∈ [𝑘 − 1, 𝑛] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑛] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧ (𝑘 ≤ 𝑛 + 1) Damit ergibt sich die Invariante der äußeren WHILE-Schleife: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ≡ [ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ª®¬ ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑛] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑛] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧ (𝑘 ≤ 𝑛 + 1) ⇐⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ≡ 𝑃(𝑘) ∧ (𝑘 ≤ 𝑛 + 1) 4.2 Invariante der inneren WHILE-Schleife Um die Invariante der inneren WHILE-Schleife 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 herzuleiten muss der Zustand der Matrix 𝜙 an den Zeitpunkten 𝑘 und 𝑖 festgehalten werden. Das Prädikat 𝑃(𝑖, 𝑘) beschreibt den Zustand der Matrix 𝜙 an den Zeitpunkten 𝑘 und 𝑖. Das Prädikat 24 4.2 Invariante der inneren WHILE-Schleife 𝑃(𝑘) kann in das Prädikat 𝑃(𝑖, 𝑘) für die Zeilen übernommen werden, die nicht von 𝑖 abhängen. Das Prädikat 𝐹𝐼𝑁 (𝑘) von 𝑃(𝑘) kann daher übernommen werden. Unter anderem fehlt es an dem Prädikat noch den Zustand der Zeilen in der Matrix festzuhalten, welche von der inneren WHILE-Schleife bereits verändert wurden und nicht mehr zum Zeitpunkt 𝑘 verändert werden. Es sind die Zeilen im Intervall von [𝑖 + 1, 𝑛], dessen Einträge in der Matrix 𝜙 den Zustand für 𝑘 + 1 darstellen. Diese Kenntnis wird aus der Nachbedingung der inneren WHILE-Schleife gewonnen, welche wie folgt definiert ist: 𝑃(𝑘 + 1) ∧ (𝑘 ≤ 𝑛) (4.3) Daher gilt für die Zeilen [𝑖 + 1, 𝑛] in 𝜙:[ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑖 ′ ∈ (𝑖, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖 − 𝑥𝑖−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧(𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) Die Zeilen im Intervall von [𝑘 − 1, 𝑖 − 1] können von 𝐼𝑁𝑇𝐸𝑅(𝑘) aus 𝑃(𝑘) übernommen werden, da diese von der inneren WHILE-Schleife zum Zeitpunkt 𝑘 noch nicht verändert wurden und daher den Zustand zum Zeitpunkt 𝑘 annehmen. Es fehlt nur noch die Zeile 𝑖 zu betrachten, welche den Zustand für 𝑘 + 1 darstellt bevor (𝑥𝑖 − 𝑥𝑖−𝑘) im nächsten Schleifendurchlauf multipliziert wird und lässt sich daher so darstellen:[ ∀𝑖′, 𝑗 ∈ [0, 𝑛] ( 𝑖 ′ = 𝑖 ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧(𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) Somit lässt sich die Invariante der inneren WHILE-Schleife 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 wie folgt definieren, wobei die Zeile 𝑖 in den zweiten Teilausdruck zusammengefasst ist: 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ≡ [ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«(𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( (𝑖′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑖) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑖, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ⇐⇒ 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ≡ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) 25 4 Konstruktion der Schleifeninvarianten Für 𝑃(𝑘) wird von nun an 𝑃(𝑛, 𝑘) verwendet mit 𝑖 = 𝑛 und damit wird: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 = 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) Jetzt muss noch geprüft werden, ob in der Initialisierung und im Endzustand des Algorithmus, 𝑃(𝑖, 𝑘) die Matrix 𝜙 zu den Zeitpunkten 𝑖, 𝑘 korrekt repräsentiert. Initialisierung der äußeren WHILE-Schleife: 𝑃(𝑛, 1) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 0) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ ∧ ( (𝑖′ ∈ [0, 𝑛 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑛) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 1 ) ∧ ( 𝑖 ′ ∈ [0, 𝑛 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′ ) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′ 𝑑=0(𝑥 𝑗 − 𝑥𝑑) = 0 ) ∧ ( 𝑖 ′ ∈ (𝑛, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( ( 𝑗 < 𝑖 ′) ∨ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 0 ) ∧ ( ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 1 ) ≡𝜙 = 𝐼𝑛+1 (4.4) 26 4.2 Invariante der inneren WHILE-Schleife Endzustand der äußeren WHILE-Schleife: 𝑃(𝑛, 𝑛 + 1) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«(′∈ [0, 𝑛) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( (𝑖′ ∈ [𝑛, 𝑛 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑛) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑛−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑛, 𝑛 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑛) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑛 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑛, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑛−1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑛−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑛) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( (𝑖′ = 𝑛) ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑛,𝑛 = ∏𝑛−1 𝑑=0(𝑥𝑛 − 𝑥𝑑)∏−1 𝑑=0(𝑥𝑛 − 𝑥𝑑) = 𝑛−1∏ 𝑑=0 (𝑥𝑛 − 𝑥𝑑) ) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑛] ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)ª®¬ (4.5) Es folgt also, dass für die Initialisierung und den Endzustand der Zustand der Matrix 𝜙 durch 𝑃(𝑖, 𝑘) korrekt beschrieben wird. 27 4 Konstruktion der Schleifeninvarianten Es ist noch hilfreich für die Verifikation der inneren WHILE-Schleife, dessen Endzustand darzustellen mit: 𝑃(𝑛, 𝑘 + 1) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«(𝑖′ ∈ [0, 𝑘) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ ∧ ( (𝑖′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑛) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑛, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑛−1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑛−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ≡∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«(𝑖′ ∈ [0, 𝑘) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ ∧ ( (𝑖′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑛) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) (4.6) Ob aber die Invarianten korrekt sind, welche momentan nur Hypothesen sind, wird sich erst beim Beweis des Algorithmus herausstellen, welcher im kommenden Abschnitt behandelt wird. 28 5 Verifikation des Algorithmus 5.1 Korrektheitsbeweis der äußeren WHILE-Schleife Im vorherigen Abschnitt wurden Hypothesen von Invarianten für die äußere und die innere WHILE-Schleife konstruiert sind korrekte Invarianten, wenn der Algorithmus mithilfe dieser Invarianten verifiziert wird. Im folgenden Unterkapitel wird zunächst unter der Annahme, dass die innere WHILE-Schleife das korrekte Ergebnis liefert und damit verifiziert ist, die äußere WHILE-Schleife verifiziert. Der Grund dafür ist, die Lesbarkeit zu vereinfachen und weil der Beweis für die Verifikation der inneren WHILE-Schleife technisch anspruchsvoller ist und ein eigenes Unterkapitel benötigt. Kommentare bei Rechnungen werden mit einem "// "gekennzeichnet. Zunächst wird die Vor- und Nachbedingung der äußeren WHILE-Schleife definiert. Vorbedingung aus 4.1: (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1) Diese Vorbedingung muss vor der Schleife gelten und das Hoare-Tripel: {𝑇𝑅𝑈𝐸}𝑘 = 1; 𝑖 = 𝑛; 𝑑 = 𝑓 ; 𝜙 = 𝐼𝑛+1{(𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1)} beschreibt die Initialisierung des Algorithmus. Mithilfe der schwächsten Vorbedingung lässt sich das Hoare-Tripel als korrekt beweisen, indem: 𝑇𝑅𝑈𝐸 ⇒ 𝑤𝑝(”𝑘 = 1; 𝑖 = 𝑛; 𝑑 = 𝑓 ; 𝜙 = 𝐼𝑛+1”, (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1)) // aus der Kompositionsregel für schwächste Vorbedingungen folgt: ⇒ 𝑤𝑝(”𝑘 = 1”, 𝑤𝑝(”𝑖 = 𝑛”, 𝑤𝑝(”𝑑 = 𝑓 ”, 𝑤𝑝(”𝜙 = 𝐼𝑛+1”, (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1))))) // aus 4.4 folgt: 𝑃(𝑛, 1) ≡ 𝜙 = 𝐼𝑛+1 // aus der Zuweisungsregel folgt: ⇒ 𝑤𝑝(”𝑘 = 1”, 𝑤𝑝(”𝑖 = 𝑛”, 𝑤𝑝(”𝑑 = 𝑓 ”, (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ (𝐼𝑛+1 = 𝐼𝑛+1)))) ⇒ 𝑤𝑝(”𝑘 = 1”, 𝑤𝑝(”𝑖 = 𝑛”, (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ ( 𝑓 = 𝑓 ) ∧ (𝐼𝑛+1 = 𝐼𝑛+1))) ⇒ 𝑤𝑝(”𝑘 = 1”, (𝑘 = 1) ∧ (𝑛 = 𝑛) ∧ ( 𝑓 = 𝑓 ) ∧ (𝐼𝑛+1 = 𝐼𝑛+1)) ⇒ (1 = 1) ∧ (𝑛 = 𝑛) ∧ ( 𝑓 = 𝑓 ) ∧ (𝐼𝑛+1 = 𝐼𝑛+1) ⇒ 𝑇𝑅𝑈𝐸 29 5 Verifikation des Algorithmus Somit gilt die Vorbedingung. Die Nachbedingung aus 4.2 lautet: 𝑃(𝑛, 𝑛 + 1) Um die Korrektheit der äußeren WHILE-Schleife zu Beweisen, wird das WHILE Theorem angewandt und liefert die Schritte für die zu erbringenden Beweise, welche die folgenden sind: 1. (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1) ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 = 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) 2. {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛)}𝑖 = 𝑛; inner; 𝑘 = 𝑘 + 1{𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } Mit inner anstelle der ausgeschriebenen inneren WHILE-Schleife aufgrund von Platz- und Lesbarkeitsgründen in diesem Unterkapitel. 3. 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ ¬(𝑘 ≤ 𝑛) ⇒ 𝑃(𝑛, 𝑛 + 1) Hier soll 1. die Verifikation der Initialisierung der WHILE-Schleife, 2. die Verifiktation des Schleifenkörpers und 3. der Abschluss der WHILE-Schleife sein. Korrektheit der Initialisierung: Die Invariante soll vor der Schleife gelten, daher die Implikation: (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1) ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 = 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) Beweis: (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ (𝑑 = 𝑓 ) ∧ 𝑃(𝑛, 1) ⇒ (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ 𝑃(𝑛, 1) // Einsetzen von (𝑘 = 1) in 𝑃(𝑛, 1) ⇒ (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ 𝑃(𝑛, 𝑘) // wegen: (𝑘 = 1) ∧ (𝑛 ≥ 0) ⇒ (𝑘 ≤ 𝑛 + 1) ⇒ (𝑘 = 1) ∧ (𝑖 = 𝑛) ∧ 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) ⇒ 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 Damit gilt die Invariante 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 vor der Schleife. Korrektheit des Schleifenkörpers: Zu beweisen ist das Hoare-Tripel: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛)}𝑖 = 𝑛; inner; 𝑘 = 𝑘 + 1{𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } welches zu 𝑇𝑅𝑈𝐸 evaluiert, wenn bei geltender Invariante 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 und Schleifenbedingung (𝑘 ≤ 𝑛) nach einem Schleifendurchlauf die Invariante 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 gilt. 30 5.1 Korrektheitsbeweis der äußeren WHILE-Schleife Zunächst lässt sich das Hoare-Tripel nach der Kompositionsregel aufteilen in die folgen- den Hoare-Tripel: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛)}𝑖 = 𝑛, inner; 𝑘 = 𝑘 + 1{𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } ⇔ {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛)}𝑖 = 𝑛{𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛)} (5.1) ∧ {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛)}inner{𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛)} (5.2) ∧ {𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛)}𝑘 = 𝑘 + 1{𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 } (5.3) Wenn die Hoare-Tripel 5.1 - 5.3 bewiesen werden, dann folgt daraus, dass das Zusammengesetzte Hoare-Tripel bewiesen ist. Um das Hoare-Tripel 5.2 zu beweisen, muss das WHILE Theorem angewandt und die damit zusammenhängende Verifikation der inneren WHILE-Schleife gezeigt werden. Dies wird erst im nächsten Unterkapitel behandelt, daher wird für die Verifikation der äußeren WHILE-Schleife angenommen, dass dieses Hoare-Tripel zu 𝑇𝑅𝑈𝐸 evaluiert. Das nächste Unterkapitel bestätigt mit der Verifikation der inneren WHILE-Schleife die Annahme und damit dann den Algorithmus im Ganzen. Also müssen hier noch 5.1 und 5.3 gezeigt werden. Beweis für 5.1: Aus dem Satz der schwächsten Vorbedingung evaluiert das Hoare-Tripel zu 𝑇𝑅𝑈𝐸 , wenn: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ⇒ 𝑤𝑝(”𝑖 = 𝑛”, 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛)) // aus der Zuweisungsregel folgt: ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑛 = 𝑛) ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ 𝑇𝑅𝑈𝐸 ⇒ 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) Es bleibt noch der Beweis für 5.3 aus: 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛) ⇒ 𝑤𝑝(”𝑘 = 𝑘 + 1”, 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ) ⇒ 𝑤𝑝(”𝑘 = 𝑘 + 1”, 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1)) // aus der Zuweisungsregel folgt: ⇒ 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 + 1 ≤ 𝑛 + 1) ⇒ 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛) Damit gilt unter der Annahme, dass die innere WHILE-Schleife verifiziert ist, die Invariante 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 vor- und nach jedem Schleifendurchlauf. Korrektheit des Abschlusses: Nun muss gezeigt werden, dass nach der äußeren WHILE-Schleife, die Matrix 𝜙 für die Ansatzfunktionen in der Newton-Basis korrekt berechnet worden ist. 31 5 Verifikation des Algorithmus Beweis: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ ¬(𝑘 ≤ 𝑛) ⇒ 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) ∧ ¬(𝑘 ≤ 𝑛) ⇒ 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) ∧ (𝑘 > 𝑛) ⇒ 𝑃(𝑛, 𝑘) ∧ (𝑘 = 𝑛 + 1) // einsetzen von (𝑘 = 𝑛 + 1) ⇒ 𝑃(𝑛, 𝑛 + 1) ∧ (𝑘 = 𝑛 + 1) ⇒ 𝑃(𝑛, 𝑛 + 1) Damit gilt: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ ¬(𝑘 ≤ 𝑛) ⇒ 𝑃(𝑛, 𝑛 + 1) Aus 4.2 folgt, dass 𝑃(𝑛, 𝑛 + 1) den Endzustand beschreibt, in dem die Ansatzfunktionen in der Newton-Basis repräsentiert sind. Die im letzten Kapitel angesprochene Bedeutung für das Einschränken von 𝑘 mit (𝑘 ≤ 𝑛 + 1) ist hier deutlich gemacht um auf die Form (𝑘 = 𝑛 + 1) zu kommen. Generell soll für Invarianten von Schleifen, die freien Variablen, welche in Prädikaten als Eingabe vorkommen, auf ihre zulässigen Eingaben beschränkt werden. Grund dafür ist, dass Korrektheitsbeweise von WHILE-Schleifen im Abschluss generell wie eben vorgestellt strukturiert sind. Da dies das Ende des Algorithmus darstellt ist der Algorithmus verifiziert worden, unter der Annahme, dass die innere WHILE-Schleife verifiziert ist. 32 5.2 Korrektheitsbeweis der inneren WHILE-Schleife 5.2 Korrektheitsbeweis der inneren WHILE-Schleife Im vorangegangenen Kapitel wurde die Verifikation des gesamten Algorithmus durchgeführt bis auf das Hoare-Tripel 5.2, welches wie folgt definiert ist: {𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟∧(𝑘 ≤ 𝑛)∧(𝑖 = 𝑛)}while(𝑖 ≥ 𝑘)𝑑 = 𝐴(𝑖, 𝑘)𝑑; 𝜙 = 𝐴(𝑖, 𝑘)−⊤; 𝑖 = 𝑖−1endwhile{𝑃(𝑛, 𝑘+1)∧(𝑘 ≤ 𝑛)} Wobei 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧(𝑘 ≤ 𝑛)∧ (𝑖 = 𝑛) die Vorbedingung und 𝑃(𝑛, 𝑘 +1)∧ (𝑘 ≤ 𝑛) die Nachbedingung der inneren WHILE-Schleife beschreiben. Durch den Beweis dieses Hoare-Tripels wird der gesamte Algorithmus verifiziert, da dies der einzige Beweisschritt ist, dessen Richtigkeit angenommen wurde und noch fehlt. Das WHILE Theorem liefert parallel zu 5.1 drei Beweisschritte, welche durchgeführt werden müssen um die innere WHILE-Schleife zu verifizieren: 1. 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛) ⇒ 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 2. {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟∧(𝑖 ≥ 𝑘)}while(𝑖 ≥ 𝑘)𝑑 = 𝐴(𝑖, 𝑘)𝑑; 𝜙 = 𝐴(𝑖, 𝑘)−⊤; 𝑖 = 𝑖−1endwhile{𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 } 3. 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ ¬(𝑖 ≥ 𝑘) ⇒ 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛) Korrektheit der Initialisierung: 𝐼𝑁𝑉𝑜𝑢𝑡𝑒𝑟 ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛) ⇒ 𝑃(𝑛, 𝑘) ∧ (𝑘 ≤ 𝑛 + 1) ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛) // durch einsetzen von (𝑖 = 𝑛) und (𝑖 = 𝑛) ∧ (𝑘 ≤ 𝑛 + 1) ⇒ (𝑖 ≥ 𝑘 − 1) // durch (𝑘 ≤ 𝑛) ∧ (𝑘 ≤ 𝑛 + 1) ⇒ (𝑘 ≤ 𝑛) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 = 𝑛) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ⇒ 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 Also gilt 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 vor dem ersten Schleifendurchlauf der inneren WHILE-Schleife und laut dem WHILE Theorem gilt beim erstmaligen Betreten der WHILE-Schleife zusätzlich noch die Schleifenbedingung, sodass: 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘) gilt. 33 5 Verifikation des Algorithmus Korrektheit des Schleifenkörpers: Das Hoare-Tripel: {𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘)}while(𝑖 ≥ 𝑘)𝑑 = 𝐴(𝑖, 𝑘)𝑑; 𝜙 = 𝐴(𝑖, 𝑘)−⊤; 𝑖 = 𝑖 − 1endwhile{𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 } soll bewiesen werden. Nach dem Satz für die schwächste Vorbedingung ist dieses Hoare-Tripel äquivalent zu: 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘) ⇒ 𝑤𝑝(”𝑑 = 𝐴(𝑖, 𝑘)𝑑; 𝜙 = 𝐴(𝑖, 𝑘)−⊤; 𝑖 = 𝑖 − 1”, 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ) // aus der Kompositionsregel für schwächste Vorbedingungen folgt: ⇒ c︷ ︸︸ ︷ 𝑤𝑝(”𝑑 = 𝐴(𝑖, 𝑘)𝑑, 𝑤𝑝(𝜙 = 𝐴(𝑖, 𝑘)−⊤, 𝑤𝑝(𝑖 = 𝑖 − 1”, 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 )︸ ︷︷ ︸ a ) ︸ ︷︷ ︸ b ) Diese schwächste Vorbedingung wird von a-c rekursiv evaluiert, sodass bei bei der Berechnung von c das Ergebnis der schwächsten Vorbedingung aller Anweisungen der inneren WHILE-Schleife steht. schwächste Vorbedingung a: 𝑤𝑝(”𝑖 = 𝑖 − 1”, 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ) = 𝑤𝑝(”𝑖 = 𝑖 − 1”, 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛)) // nach dem Satz der schwächsten Vorbedingung folgt: = 𝑃(𝑖 − 1, 𝑘) ∧ (𝑖 − 1 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) (5.4) = 𝑃(𝑖 − 1, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) (5.5) schwächste Vorbedingung b: 𝑤𝑝(𝜙 = 𝐴(𝑖, 𝑘)−⊤𝜙, 𝑤𝑝(”𝑖 = 𝑖−1”, 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 )) 5.4 = 𝑤𝑝(𝜙 = 𝐴(𝑖, 𝑘)−⊤𝜙, 𝑃(𝑖−1, 𝑘)∧(𝑖−1 ≥ 𝑘−1)∧(𝑘 ≤ 𝑛)) Da das Prädikat 𝑃(𝑖 − 1, 𝑘) die Einträge in der Matrix 𝜙 beschreibt, werden sie ersetzt durch das Ergebnis der Matrizenmultiplikation von 𝜙 = 𝐴(𝑖, 𝑘)−⊤: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝜙𝑖′ , 𝑗 = 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 34 5.2 Korrektheitsbeweis der inneren WHILE-Schleife 𝑃(𝑖 − 1, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) nimmt nach der obigen Ersetzung folgende Form an: = ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ (5.6) ∧ ( ((𝑖′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑖 − 1)) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) (5.7) ∧ ( (𝑖′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 > 𝑖 ′)) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) (5.8) ∧ ( 𝑖 ′ ∈ (𝑖 − 1, 𝑛] ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) (5.9) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) Um die oben-stehenden Summen zu berechnen, ist es Hilfreich eine Fallunterscheidung der verschiedenen Werte durchzuführen, die die Einträge der Matrix 𝐴(𝑖, 𝑘)−⊤ besitzen können: ∀𝑖′ ∈ [0, 𝑛] : 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) =  𝑥𝑖′ − 𝑥𝑖′−𝑘 für (𝑖 = 𝑖 ′) ∧ (𝑑 = 𝑖) 1 für ((𝑖′ = 𝑑) ∧ (𝑑 ≠ 𝑖)) ∨ ((𝑖′ = 𝑖 − 1) ∧ (𝑖 = 𝑑)) 0 sonst (5.10) Jetzt können die Teilausdrücke 5.6-5.9 jeweils so aufgeteilt werden, sodass die Summe∑𝑛 𝑑=0 𝐴 −𝑇 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 nur die drei folgenden Ergebnisse hat: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑖 ′ ∉ {𝑖 − 1, 𝑖} ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 ) ∧ ( 𝑖 ′ = 𝑖 − 1 ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖−1, 𝑗 + 𝜙𝑖, 𝑗 = 𝜙𝑖′ , 𝑗 + 𝜙𝑖′+1, 𝑗 ) ∧ ( 𝑖 ′ = 𝑖 ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = (𝑥𝑖 − 𝑥𝑖−𝑘)𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘)𝜙𝑖′ , 𝑗 ) Dies folgt aus der Überlegung in 5.10, dass die Zeilen in der Matrix 𝐴(𝑖, 𝑘)−⊤, welche nicht {𝑖 − 1, 𝑖} sind, die Zeilen einer Einheitsmatrix darstellen und für die Zeilen {𝑖 − 1, 𝑖} jeweils eine Transformation der Basispolynome durchgeführt wird. Nun werden die Summen für die Teilausdrücke jeweils berechnet und am werden dann nach 𝜙𝑖′ , 𝑗 aufgelöst, Zusammengefasst und vereinfacht: 35 5 Verifikation des Algorithmus Teilausdruck 5.6 Für den Fall 𝑖′ ∈ [0, 𝑘 − 1) ist 𝑖′ ∉ {𝑖 − 1, 𝑖}, da (𝑖 ≥ 𝑘) gilt, also: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝑖 ′ ∈ [0, 𝑘 − 1) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Für 𝑗 < 𝑖 ′ muss eine Fallunterscheidung zwischen ( 𝑗 > 𝑖 ′) und ( 𝑗 = 𝑖 ′) gemacht werden: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑗 < 𝑖 ′) ∧ (𝑖′ ∉ {𝑖 − 1, 𝑖}) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑗 < 𝑖 ′) ∧ (𝑖′ = 𝑖 − 1) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 + 𝜙𝑖′+1, 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) − 𝜙𝑖′+1, 𝑗 // aus ( 𝑗 < 𝑖 ′ + 1) ⇒ 𝜙𝑖′+1, 𝑗 = 𝑖 ′∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 0 folgt: ⇔ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑗 < 𝑖 ′) ∧ (𝑖′ = 𝑖) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = (𝑥𝑖′−1 − 𝑥𝑖′−𝑘)𝜙𝑖′ , 𝑗 = 𝑖 ′∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) (𝑥𝑖′ − 𝑥𝑖′−𝑘) // aus ( 𝑗 < 𝑖 ′ + 1) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 0 folgt: ⇔ 𝜙𝑖′ , 𝑗 = 0 ⇔ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Somit lässt sich zusammenfassen: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ 36 5.2 Korrektheitsbeweis der inneren WHILE-Schleife Teilausdruck 5.7 Für 𝑖′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 = 𝑖 ′) ist 𝑖′ ∉ {𝑖 − 1, 𝑖}, da (𝑖 ≥ 𝑘) gilt, also: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Für (𝑖′ = 𝑖 − 1) muss auch eine Fallunterscheidung zwischen ( 𝑗 > 𝑖 ′) und ( 𝑗 = 𝑖 ′) gemacht werden: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : (𝑖′ = 𝑖 − 1) ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 + 𝜙𝑖′+1, 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) − 𝜙𝑖′+1, 𝑗 // aus ( 𝑗 = 𝑖 ′) ⇒ ( 𝑗 < 𝑖 ′ + 1) ⇒ 𝜙𝑖′+1, 𝑗 = 𝑖 ′∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 0 folgt: ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) 37 5 Verifikation des Algorithmus ∀𝑖′, 𝑗 ∈ [0, 𝑛] : (𝑖′ = 𝑖 − 1) ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 + 𝜙𝑖′+1, 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) − 𝜙𝑖′+1, 𝑗 // aus ( 𝑗 > 𝑖 ′) ∧ (𝑖′ + 1 = 𝑖) ⇒ 𝜙𝑖′+1, 𝑗 = ∏𝑖 ′ 𝑑=0(𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) folgt: ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) − ∏𝑖 ′ 𝑑=0(𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) // Ersten Bruch um (𝑥 𝑗 − 𝑥𝑖′−𝑘+1) erweitern: // (𝑥 𝑗 − 𝑥𝑖′ ) aus 𝑖 ′∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ausklammern: ⇔ 𝜙𝑖′ , 𝑗 = (∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) · (𝑥 𝑗 − 𝑥𝑖′−𝑘+1)(∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) · (𝑥 𝑗 − 𝑥𝑖′−𝑘+1) − (∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) · (𝑥 𝑗 − 𝑥𝑖′ )∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = (∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) · (𝑥 𝑗 − 𝑥𝑖′−𝑘+1)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) − (∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) · (𝑥 𝑗 − 𝑥𝑖′ )∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) // Durch ausklammern von ( 𝑥 𝑗 − 𝑥𝑖′−𝑘+1 − (𝑥 𝑗 − 𝑥𝑖′ ) ) ergibt sich: ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) · ( 𝑥 𝑗 − 𝑥𝑖′−𝑘+1 − (𝑥 𝑗 − 𝑥𝑖′ ) ) ⇔ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Die Ergebnisse für den zweiten Teilausdruck fassen sich wie folgt zusammen: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ( 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ( (𝑖′ = 𝑖 − 1) ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) · 𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) Teilausdruck 5.8 Für 𝑖′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 > 𝑖 ′) ist 𝑖′ ∉ {𝑖 − 1, 𝑖}, da (𝑖 ≥ 𝑘) gilt, also: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝑖 ′ ∈ [𝑘−1, 𝑖−2]∧( 𝑗 > 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘)·𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = (𝑥𝑖′−𝑥𝑖′−𝑘+1)· ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) 38 5.2 Korrektheitsbeweis der inneren WHILE-Schleife Teilausdruck 5.9 Für 𝑖′ ∈ (𝑖, 𝑛] ist 𝑖′ ∉ {𝑖 − 1, 𝑖}, also: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝑖 ′ ∈ (𝑖, 𝑛]∧( 𝑗 ≥ 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘) ·𝜙𝑑, 𝑗 = 𝜙𝑖′ , 𝑗 = (𝑥𝑖′−𝑥𝑖′−𝑘) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Für (𝑖′ = 𝑖) ∧ ( 𝑗 ≥ 𝑖 ′) gilt: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : (𝑖′ = 𝑖)∧( 𝑗 ≥ 𝑖 ′) ⇒ 𝑛∑︁ 𝑑=0 𝐴−⊤ 𝑖 ′ ,𝑑 (𝑖, 𝑘)·𝜙𝑑, 𝑗 = (𝑥𝑖′−𝑥𝑖′−𝑘)·𝜙𝑖′ , 𝑗 = (𝑥𝑖′−𝑥𝑖′−𝑘)· ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) (𝑥𝑖′ − 𝑥𝑖′−𝑘) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ⇔ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) Wenn die Ergebnisse der Teilausdrücke 5.6-5.9 zusammengefasst werden, lässt sich 𝑤𝑝(”𝜙 = 𝐴(𝑖, 𝑘)−⊤𝜙”, 𝑃(𝑖 − 1) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛)) wie folgt darstellen:[ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( (𝑖′ = 𝑖 − 1) ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 2] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑖, 𝑛] ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) · ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( (𝑖′ = 𝑖) ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) )] ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) 39 5 Verifikation des Algorithmus Nach dem Vereinfachen folgt:[ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : ©­«𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ ∧ ( (𝑖′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑖) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘 − 1, 𝑖 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑖, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ] ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) Das Prädikat in den eckigen Klammern ist genau das Prädikat 𝑃(𝑖, 𝑘), also gilt: 𝑤𝑝(”𝜙 = 𝐴(𝑖, 𝑘)−⊤𝜙”, 𝑃(𝑖 − 1, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛)) = 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) (5.11) schwächste Vorbedingung c: 𝑤𝑝(”𝑑 = 𝐴(𝑖, 𝑘)𝑑, 𝑤𝑝(𝜙 = 𝐴(𝑖, 𝑘)−⊤, 𝑤𝑝(𝑖 = 𝑖−1”, 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ))) 5.11 = 𝑤𝑝(”𝑑 = 𝐴(𝑖, 𝑘)𝑑”, 𝑃(𝑖, 𝑘)∧(𝑖 ≥ 𝑘)∧(𝑘 ≤ 𝑛)) Weil für die Zuweisung 𝑑 = 𝐴(𝑖, 𝑘)𝑑 kein 𝑑 frei in 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) vorkommt, ist: 𝑤𝑝(”𝑑 = 𝐴(𝑖, 𝑘)𝑑”, 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛)) = 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) Somit muss nur noch gezeigt werden, dass 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛): 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ (𝑖 ≥ 𝑘) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 ≥ 𝑘) // wegen (𝑖 ≥ 𝑘 − 1) ∧ (𝑖 ≥ 𝑘) ⇒ (𝑖 ≥ 𝑘) gilt: ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘) ∧ (𝑘 ≤ 𝑛) Damit evaluiert das Hoare-Tripel zu 𝑇𝑅𝑈𝐸 und die Schleifeninvariante gilt vor- und nach dem Ausführen der inneren WHILE-Schleife. Es bleibt nur noch zu zeigen, dass beim Verlassen der inneren WHILE-Schleife der Zustand der Matrix 𝜙 für die Schleifenvariable 𝑘 + 1 gilt. 40 5.2 Korrektheitsbeweis der inneren WHILE-Schleife Korrektheit des Abschlusses Schließlich muss noch gezeigt werden, dass: 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ ¬(𝑖 ≥ 𝑘) ⇒ 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛) 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ ¬(𝑖 ≥ 𝑘) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ∧ ¬(𝑖 ≥ 𝑘) ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 ≥ 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) ∧ (𝑖 < 𝑘) // aus (𝑖 ≥ 𝑘 − 1) ∧ (𝑖 < 𝑘) ⇒ (𝑖 = 𝑘 − 1) folgt: ⇒ 𝑃(𝑖, 𝑘) ∧ (𝑖 = 𝑘 − 1) ∧ (𝑘 ≤ 𝑛) // einsetzen von (𝑖 = 𝑘 − 1) in 𝑃(𝑖, 𝑘) ⇒ 𝑃(𝑘 − 1, 𝑘) ∧ (𝑘 ≤ 𝑛) Für 𝑃(𝑘 − 1, 𝑘) ∧ (𝑘 ≤ 𝑛) ergibt sich: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : [©­«(𝑖′ ∈ [0, 𝑘 − 1) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( ((𝑖′ ∈ [𝑘, 𝑘 − 2] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑘 − 1)) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( (𝑖′ ∈ [𝑘, 𝑘 − 2] ∧ ( 𝑗 > 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘+1) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘+1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ (𝑘 − 1, 𝑛] ∧ ( 𝑗 ≥ 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) )] ∧ (𝑘 ≤ 𝑛) Die Intervalle für das 𝑖′ im zweiten und dritten Teilausdruck sind leer, daher stimmt die Implikation und die Teilausdrücke können wegfallen, bis auf die Bedingung (𝑖′ = 𝑘 − 1), welche durch Folgende Überlegung in den ersten Teilausdruck absorbiert werden kann: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : 𝑖 ′ = 𝑘 − 1 ⇒ 𝜙𝑖′ , 𝑗 ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) Der vierte Teilausdruck wird in die Fälle 𝑗 = 𝑖 ′ und 𝑗 > 𝑖 ′ unterteilt. Damit folgt: ∀𝑖′, 𝑗 ∈ [0, 𝑛] : [©­«(𝑖′ ∈ [0, 𝑘) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗) ª®¬ ∧ ( 𝑖 ′ ∈ [𝑘, 𝑛] ∧ ( 𝑗 = 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) )] ∧ ( 𝑖 ′ ∈ [𝑘, 𝑛] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) )] ∧ (𝑘 ≤ 𝑛) 41 5 Verifikation des Algorithmus Weil es keine Einträge in der Matrix für (𝑖′ = 𝑛) ∧ ( 𝑗 > 𝑖 ′) gibt, kann das Intervall vom dritten Teilausdruck auf [𝑘, 𝑛 − 1] verkürzt werden und der zweite Teilausdruck in einer anderen Form notiert werden: ≡ ∀𝑖′, 𝑗 ∈ [0, 𝑛] : [ ©­«(𝑖′ ∈ [0, 𝑘) ∨ ( 𝑗 < 𝑖 ′)) ⇒ 𝜙𝑖′ , 𝑗 = 𝑖 ′−1∏ 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) = 𝜋𝑖′ (𝑥 𝑗)ª®¬ ∧ ( (𝑖′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 = 𝑖 ′)) ∨ (𝑖′ = 𝑛) ⇒ 𝜙𝑖′ , 𝑗 = ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) ) ∧ ( 𝑖 ′ ∈ [𝑘, 𝑛 − 1] ∧ ( 𝑗 > 𝑖 ′) ⇒ 𝜙𝑖′ , 𝑗 = (𝑥𝑖′ − 𝑥𝑖′−𝑘) ∏𝑖 ′−1 𝑑=0 (𝑥 𝑗 − 𝑥𝑑)∏𝑖 ′−𝑘 𝑑=0 (𝑥 𝑗 − 𝑥𝑑) )] ∧ (𝑘 ≤ 𝑛) Aus 4.6 folgt, dass das Prädikat in den eckigen Klammern das Prädikat 𝑃(𝑛, 𝑘 + 1) darstellt, also: 𝐼𝑁𝑉𝑖𝑛𝑛𝑒𝑟 ∧ ¬(𝑖 ≥ 𝑘) ⇒ 𝑃(𝑛, 𝑘 + 1) ∧ (𝑘 ≤ 𝑛) Damit erfüllen sich alle Anforderungen des WHILE Theorems für die Verifikation der inneren WHILE-Schleife. Da im vorangegangenen Kapitel bereits gezeigt wurde, dass der Algorithmus verifiziert ist unter der Annahme, die innere WHILE-Schleife sei verifiziert, der Algorithmus nun vollständig verifiziert. Dazu gehört auch, dass die dividierten Differenzen verifiziert sind, was aus der Überlegung in Kapitel 3 folgt, weil sich das zu interpolierende Polynom nicht verändert. 42 6 Diskussion und Ausblick In dieser Bachelorarbeit wurde der newtonsche Ansatz für die Interpolation verifiziert, wobei sich der Beweis nur auf die Verifikation der Ansatzfunktionen beschränkt. Trotzdem wird damit die Richtigkeit der dividierten Differenzen bewiesen, was eine andere Herangehensweise für die Verifikation des newtonschen Ansatzes für die Interpolation ist als Philip Urban mit seiner Bachelorarbeit [Urb21], dessen Beweis sich auf die dividierten Differenzen bezogen hat. Der nächste Schritt wäre es, weitere Algorithmen zur Interpolation mit den vorgestellten Techniken zu verifizieren und herauszufinden, inwiefern sich die einzelnen Überlegungen dieser Bachelorarbeit auf diese Algorithmen übertragen. Für die Herleitung des Basiswechsels ist es einfach die Basistransformationen zu bestimmen, indem die Matrizenschreibweise gewählt wird und nur das Inverse einer Matrix berechnet wird. Die Konstruktion der Schleifeninvarianten ist sehr abhängig von den ausgeführten Anweisungen aber es ist immer Hilfreich sich die Vor- und Nachbedingungen zu berücksichtigen, da diese in irgendeiner Form in der Invariante auftreten müssen. Außerdem benötigen die Invarianten Einschränkungen auf den Umfang der in ihr vorkommenden Variablen, was in dieser Bachelorarbeit ersichtlich wurde. Die Korrektheitsbeweise lassen sich bis auf die Hoare-Tripel gut auf andere Algorithmen übertragen, da die Hoare-Tripel in den WHILE-Schleifen stark vom Algorithmus abhängen. An diesem Beweis wird deutlich, dass kurze Algorithmen aus der Numerik sich durchaus für einen Korrektheitsbeweis eignen, anstelle von einem herkömmlichen Test, welcher kein formaler Beweis ist. Literaturverzeichnis [BH16] R. Bubel, R. Hähnle. „KeY-Hoare“. In: Deductive Software Verification – The KeY Book: From Theory to Practice. Hrsg. von W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, M. Ulbrich. Cham: Springer International Publishing, 2016, S. 571–589 (zitiert auf S. 7). [Gan05] W. Gander. „Change of basis in polynomial interpolation“. In: Numerical Linear Algebra with Applications 12 (2005) (zitiert auf S. 7). [MG20] M. E. Myers, R. A. van de Geijn. LAFF-On Programming for Correctness. 2020 (zitiert auf S. 7, 9). [Urb21] P. Urban. „Formale Verifikation von Basistransformationen für Funktionsdarstellun- gen“. In: (2021) (zitiert auf S. 7, 43). [ZZW+13] L. Zou, N. Zhany, S. Wang, M. Fränzle, S. Qin. „Verifying simulink diagrams via a hybrid hoare logic prover“. In: 2013 Proceedings of the International Conference on Embedded Software (EMSOFT). IEEE. 2013, S. 1–10 (zitiert auf S. 7). Erklärung Ich versichere, diese Arbeit selbstständig verfasst zu haben. Ich habe keine anderen als die angegebenen Quellen benutzt und alle wörtlich oder sinngemäß aus anderen Werken übernommene Aussagen als solche gekennzeichnet. Weder diese Arbeit noch wesentliche Teile daraus waren bisher Gegenstand eines anderen Prüfungsverfahrens. Ich habe diese Arbeit bisher weder teilweise noch vollständig veröffentlicht. Das elektronische Exemplar stimmt mit allen eingereichten Exemplaren überein. Ort, Datum, Unterschrift 1 Einleitung 2 Grundlagen 3 Herleitung des Basiswechsels 4 Konstruktion der Schleifeninvarianten 4.1 Invariante der äußeren WHILE-Schleife 4.2 Invariante der inneren WHILE-Schleife 5 Verifikation des Algorithmus 5.1 Korrektheitsbeweis der äußeren WHILE-Schleife 5.2 Korrektheitsbeweis der inneren WHILE-Schleife 6 Diskussion und Ausblick Literaturverzeichnis