Diese Dissertation beschreibt die automatische Erzeugung korrekter Spezifikationen aus einem gegebenen Programm in Form von Schleifeninvarianten und Methodenverträge. Korrekte Spezifikationen sind für die Analyse nichttrivialer Programme unumgänglich. Verifikationswerkzeuge können komplexe Eigenschaften von realen Programmen beweisen, benötigen aber hierzu korrekte Spezifikationen für unbeschränkte Schleifen und unbeschränkte rekursive Methodenaufrufe. Selbst das Fehlen einer einzigen Spezifikation kann dazu führen, dass der Beweis nicht geschlossen werden kann.

Im Allgemeinen sind Automatisierung und Präzision Ziele, die sich oft gegenseitig ausschließen. Die Herausforderung besteht häufig darin einen guten Mittelweg zu finden. Um vollautomatische Erzeugung von Spezifikationen zu erlangen, müssen Kompromisse bei der Präzision hingenommen werden. Es existieren Ansätze, die Programme als Ganzes abstrahieren, indem alle Typen durch abstrakte Typen ersetzt werden, die nur endlich viele abstrakte Werte beinhalten. Dies ermöglicht es bei der automatischen Spezifikationserzeugung Algorithmen zu verwenden, die auf Fixpunktberechnung beruhen, und so deren Terminierung zu garantieren. Bei den bisherigen Ansätzen tritt ein Präzisionsverlust nicht nur bei Schleifen oder Methodenaufrufen auf, bei denen dieses zum Sicherstellen der Automatisierung notwendig ist, sondern im gesamten Programm.

Die in dieser Dissertation vorgestellte Spezifikationserzeugung zeichnet sich durch folgende Punkte aus: (i) Abstraktion findet nur bei Schleifen und Methodenaufrufen statt, so dass Präzision an allen anderen Stellen des Programms beibehalten wird, (ii) durch das Koppeln der Abstraktion an die Einführung neuer Invarianten wird eine präzisere Darstellung des symbolischen Programmzustandes erreicht, und (iii) werden komplexere Konstrukte zur Steuerung des Kontrollflusses realer Programmiersprachen unterstützt, anstatt sich auf einer akademischen Spielsprache zu beschränken.

Um den Präzisionsverlust zu minimieren, werden Programmzustände abstrahiert, an Stelle ganzer Programme. Um die Terminierung der Fixpunktalgorithmen sicherzustellen, müssen Programmzustände bei Schleifen oder Methodenaufrufen abstrahiert werden. Die Abstraktion von Programmzuständen wird mittels abstrakter Domänen passenden Typs ausgeführt. Diese abstrakten Werte können dann ausserhalb der Schleife oder des Methodenaufrufs als normale Werte betrachtet werden, für die nur Teilwissen zur Verfügung steht. Reale Programmiersprachen wie Java beinhalten zum Beispiel sowohl einen Programm-Heap, der von Schleifen oder Methodenaufrufen verändert werden kann, als auch Objekte und Arrays als Typen neben den Primitivtypen wie Bool'sche Werte oder ganze Zahlen. Abstrakte Domänen für Objekte und Programm-Heaps werden vorgestellt.

Da abstrakte Domänen sich nur schwer problemspezifisch anpassen lassen, werden zusätzliche Invarianten beim Abstrahieren eingeführt, um den Folgen der Überapproximation etwas entgegenzuarbeiten. Dies erlaubt es zum Beispiel Wissen über die Werte der Elemente eines Arrays beizubehalten, die ansonsten bei der Durchführung der Abstraktion verloren gegangen wären.

Reale Programmiersprachen beinhalten viele Konstrukte, die die automatische Spezifikationserzeugung erschweren. Sowohl bei Schleifen als auch bei einfacher Rekursion ist die automatische Spezifikationserzeugung vergleichsweise einfach zu realisieren. Kompliziertere Fälle, wie zum Beispiel wechselseitige Rekursion, stellen die automatische Spezifikationserzeugung vor signifikant größere Herausforderungen. Auch nichtstandard Kontrollflüsse, wie das Verlassen einer Schleife durch ein break, das Werfen einer Exception oder das Verlassen einer Methode innerhalb einer Schleife, sind weitere Komplikationen bei der automatischen Spezifikationserzeugung. Das in dieser Dissertation entwickelte Verfahren kann für alle diese Fälle korrekte Spezifikationen automatisch erzeugen.