Automatische Synthese rekursiver Programme als Beweisverfahren

In diesem Buch wird ein Verfahren vorgestellt, mit dem

Induktionsbeweise vonExistenzaussagen automatisch gef}hrt

werden k|nnen. Es ist ein deduktives

Programmsyntheseverfahren, das ausgehend von

Existenzaussagen, die als formale Programmspezifikationen

aufgefa~t werden, rekursive Programme erzeugt. Kann ein

solches Programm korrekt erstellt werden, so beschreibt der

Syntheseproze~ gleichzeitig einen Induktionsbeweis der

entsprechenden Existenzaussage.

Auf der Basis dieses Verfahrens wurde ein automatisches

Programmsynthesesystem entwickelt und implementiert. Es

verwendet spezielle Transformationsregeln sowie Strategien

und Heuristiken, die die Beweissuche steuern. Sie werden

anhand vieler Beispiele ausf}hrlich diskutiert.

Obwohl die hier beschriebene Methode in erster Linie zur

Automatisierung von Existenzbeweisen entwickelt worden ist,

und der Aspekt der automatischen Softwareentwicklung eher im

Hintergrund steht, motivieren zahlreiche Beispiele dazu, das

Verfahren auch f}r diesen Zweck einzusetzen.