Automatische Synthese Rekursiver Programme Als Beweisverfahren |
|
Author:
| Biundo, Susanne |
Series title: | Informatik-Fachberichte Ser. |
ISBN: | 978-3-540-55300-7 |
Publication Date: | Apr 1992 |
Publisher: | Springer Berlin / Heidelberg
|
Imprint: | Springer |
Book Format: | Paperback |
List Price: | USD $69.99USD $69.99 |
Book Description:
|
In diesem Buch wird ein Verfahren vorgestellt, mit demInduktionsbeweise vonExistenzaussagen automatisch gef}}hrtwerden k|nnen. Es ist ein deduktivesProgrammsyntheseverfahren, das ausgehend vonExistenzaussagen, die als formale Programmspezifikationenaufgefa~t werden, rekursive Programme erzeugt. Kann einsolches Programm korrekt erstellt werden, so beschreibt derSyntheseproze~ gleichzeitig einen Induktionsbeweis derentsprechenden Existenzaussage.Auf der Basis dieses Verfahrens wurde ein...
More DescriptionIn diesem Buch wird ein Verfahren vorgestellt, mit demInduktionsbeweise vonExistenzaussagen automatisch gef}}hrtwerden k|nnen. Es ist ein deduktivesProgrammsyntheseverfahren, das ausgehend vonExistenzaussagen, die als formale Programmspezifikationenaufgefa~t werden, rekursive Programme erzeugt. Kann einsolches Programm korrekt erstellt werden, so beschreibt derSyntheseproze~ gleichzeitig einen Induktionsbeweis derentsprechenden Existenzaussage.Auf der Basis dieses Verfahrens wurde ein automatischesProgrammsynthesesystem entwickelt und implementiert. Esverwendet spezielle Transformationsregeln sowie Strategienund Heuristiken, die die Beweissuche steuern. Sie werdenanhand vieler Beispiele ausf}}hrlich diskutiert.Obwohl die hier beschriebene Methode in erster Linie zurAutomatisierung von Existenzbeweisen entwickelt worden ist,und der Aspekt der automatischen Softwareentwicklung eher imHintergrund steht, motivieren zahlreiche Beispiele dazu, dasVerfahren auch f}}r diesen Zweck einzusetzen.