Computational logic and quantifier elimination techniques for (semi-)automatic static analysis and synthesis of algorithms / eingereicht von: Mǎdǎlina Erascu

• VerfasserIn: Erascu, Mǎdǎlina
• Place / Publishing House: 2012
• Year of Publication: 2012
• Language: English
• Classification: 31.76 - Numerische Mathematik; 54.10 - Theoretische Informatik; 31.10 - Mathematische Logik. Mengenlehre
• Physical Description: VIII, 109, 4 S.
• Notes: Zsfassung in dt. und engl. Sprache

ger: In dieser Arbeit werden logische und algebraische Zug\"ange zur Analyse von imperativenrekursiven Algorithmen sowie zur Synthese von optimalen Algorithmen pr\"asentiert.<br />Zun\"achst entwickeln und formalisieren wir eine Methode zur Verifikation von imperativenrekursiven Programmen, die automatisch mit dem System {\em Theorema} bewiesen wird. Unser Ziel ist es das minimale logische Ger\"ust zu bestimmen, das notwendig ist um eine kor\-rekte Sammlung von Methoden f\"ur Programmverifikation zu formulieren und (computerunterst\"utzt) zu beweisen. Unsere Arbeit zeigt, dass f\"ur das Schlu\ss folgern\"uber Programme nicht notwendigerweise eine komplexe theoretische Konstruktion ben\"otigt wird, da es m\"oglich ist die Semantik des Programms in die Semantik logischer Formeln\"uberzuf\"uhren und damit spezielle Theorien \"uber die Exekution von Programmenvermieden werden k\"onnen. Die Semantik wird, in der Objekttheorie, als implizite Definition der Funktion, die durch das Programm implementiert ist, dargestellt. Termination, ebenfalls in der Objekttheorie definiert, ist ein Induktionsprinzip gebildetvon der Struktur des Programms bez\"uglich iterativer Strukturen (rekursive Aufrufe und exttt{\underline{while}}-Schleifen). Eine Objekttheorie ist die Theorie \"uber die Pr\"adikate, Konstanten und Funktionen, die im Programmtext vorkommen. Derzeit kann unsere Methode auf Programme mit einer einfachen Rekursion und mit beliebig verschachtelten Schleifen mit abruptem Abbruch ( exttt{\underline{break}}, exttt{\underline{return}}) angewandt werden.<br />Im zweiten Teil untersuchen wir Methoden zur Synthese von optimalen Algorithmen. Als ein Fallbeispiel betrachten wir das Quadratwurzelproblem:<br />gegeben eine reelle Zahl~$x$ undeine Fehlerschranke~$\varepsilon$, ist eine reelles Intervall zu bestimmen, das~$x$ enth\"alt und dessen L\"ange kleiner als~$\varepsilon$ ist. Als Schema f\"ur den Algorithmus verwenden wir iterative Verfeinerung: der Algorithmus startet mit einem Anfangsintervall, das wiederholt aktualisiert wird durch die Anwendung einer Verfeinerungsabbildung, nennen wir sie~$f$, solange bis es klein genug ist. In diesem Fall entspricht die Synthese dem Bestimmen einer Verfeinerungsabbildung~$f$, die sicher stellt, dass der Algorithmus korrekt ist (schleifeninvariant), terminiert (kontrahierend) und optimal ist. Diese Anforderungen k\"onnen als Quantoreneliminationsproblem \"uber den reellen Zahlen formuliert werden. Daher k\"onnte das Problem laut Theorie automatischgel\"ost werden. In der Praxis sind die Rechenanforderungen zu immens und somit ist die automatische Synthese derzeit mit der aktuell verf\"ugbaren Software f\"ur Quantorenelimination nicht durchf\"uhrbar. Deshalb wurden einige Umformungsschritte von Hand ausgef\"uhrt und wir haben in einem semi-automatischen Prozess optimale Algorithmen (unter nat\"urlichen Vor\-aus\-setzungen) synthetisiert.<br />

eng: This thesis presents logical and algebraic approaches for analyzing imperative recursive algorithms and for synthesizing optimal algorithms.<br />First we develop, formalize, and prove automatically, in the \emph{Theorema} system, the soundness of a method for the verification of imperative recursive programs. Our goal is to identify the minimal logical apparatus necessary for formulating and proving (in computer-assisted manner) a correct collection of methods for program verification. Our work shows that reasoning about programs does not necessarily need a complex theoretical construction, because it is possible to transfer the semantics of the program into the semantics of logical formulas, thus avoiding any special theory related to program execution. We express the semantics as an implicit definition, in the object theory, of the function implemented by the program. Termination, defined also in the object theory, is an induction principle developed from the structure of the program with respect to iterative structures (recursive calls and exttt{\underline{while}} loops). An object theory is the theory relevant to the predicates, constants, and functions occurring in the program text.<br />Currently, our method can be applied to programs with single recursion and with arbitrarily-nested loops with abrupt termination ( exttt{\underline{break}}, exttt{\underline{return}}).<br />Second we investigate methods for synthesizing optimal algorithms. As a case study, we consider the square root problem: given the real number $x$ and the error bound $\varepsilon$, find a real interval such that it contains $\sqrt{x}$ and its width is less than $\varepsilon$. We use iterative refining as algorithm schema: the algorithm starts with an initial interval and repeatedly updates it by applying a refinement map, say $f,$ on it until it becomes narrow enough. Then the synthesis amounts to finding a refinement map $f$ that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these could be formulated as quantifier elimination over the real numbers. Hence, in principle, they could be performed automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general quantifier elimination software. Therefore, we performed some hand derivations and were able to synthesize semi-automatically optimal algorithms under natural assumptions.