Formale Verifikation von Basistransformationen für Funktionsdarstellungen

Abstract

Die vorliegende Bachelorarbeit gibt einen Einblick in die Anwendung der axiomatischen Semantik auf Algorithmen der Numerik. Dabei wurde das Hoare-Kalkül auf drei Algorithmen der Polynominterpolation angewendet. Untersucht wurden zwei Varianten des Algorithmus von Aitken-Neville und der newtonsche Algorithmus. Gesucht wurden Formalismen und Umformungstechniken, die auf Basistransformationen für Algorithmen aus der Numerik übertragen werden können. Die Anwendungen zeigen eine Zweckmäßigkeit der axiomatischen Semantik für numerische Algorithmen.