Invarianten von Ansatzfunktionen beim Basiswechsel

Abstract

Diese Bachelorarbeit beschäftigt sich mit der formalen Verifikation des newtonschen Ansatzes für die Interpolation mithilfe des Hoare-Kalküls. Hierfür werden zunächst die Grundlagen des Hoare-Kalküls erörtert. Daraufhin wird der Algorithmus so verändert, sodass neben der Berechnung der führenden Koeffizienten, die Ansatzfunktionen durch einen Wechsel in der Basis berechnet werden. Für die im angepassten Algorithmus vorkommenden WHILE-Schleifen werden systematisch Hypothesen für Invarianten hergeleitet und finden für den darauf folgenden Beweis Anwendung. Bewiesen wird die Korrektheit der berechneten Ansatzfunktionen. In dieser Bachelorarbeit wird auch gezeigt, dass das Verifizieren der Ansatzfunktionen auch die Korrektheit der berechneten führenden Koeffizienten beweist. Daraus folgt die formale Verifikation des Algorithmus. Es wird auch erörtert inwiefern sich Herangehensweisen für den Beweis und Umformungen des Algorithmus auf andere Algorithmen in der Numerik übertragen lassen.