 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Beispielanwendung Amphion |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Ein weit verbreitetes Problem in der Softwareentwicklung ist das mangelnde Wissen über bereits vorhandene Dinge. Oft werden Routinen immer und immer wieder neu geschrieben, obwohl sie in einer Library zur Verfügung stehen. Amphion ist ein Projekt der NASA um dem entgegen zu wirken. Mit Amphion ist es möglich Fortran-Programme zu entwickeln auf Basis der JPL SPICELIB ohne Kenntnis über deren Möglichkeiten zu haben. Amphion ist ein System um Softwarewiederverwendung zu automatisieren. Dabei gibt der Benutzer, oder besser Entwickler, nur eine Spezifikation dessen, was er haben möchte und Amphion generiert automatisch den zugehörigen Code. Amphion verwendet einen Automatischen Beweiser um eine korrekte Synthese der Programme zu garantieren. Amphion benutzt Subroutinen aus der Library anstatt, der elementaren Befehle von Fortran. Dies in Kombination mit auf den Anwendungsbereich zugeschnittenen Kontrollstrategien ermöglicht es, Automatisches Beweisen sinnvoll einzusetzen um Programme zu synthetisieren.1 2
Amphion bietet dem Benutzer die Möglichkeit über eine graphische Eingabe ein System zu modellieren. Dies wird dann automatisch in Prädikaten-Logik erster Ordnung übersetzt und dem darunterliegenden Automatischen Beweiser  SNARK übergeben. Die verwendete Komponente um die endgültige Übersetzung in Fortran vorzunehmen kann, laut angaben der Entwickler, leicht ausgetauscht werden, so dass es durchaus denkbar ist eine Übersetzung in eine andere Zielsprache vorzunehmen. Die Übersetzung der Eingaben, die über das graphische Interface gemacht werden, ist nur eine Teilmenge der Prädikaten-Logik erster Ordnung. Jedoch ist es offen gelassen worden, dass erfahrene Benutzer Eingaben direkt in der Logik vornehmen, so das die Prädikaten-Logik erster Ordnung zur Verfügung steht.
Der Konstruktionsvorgang geschieht nun folgendermaßen: Es wird angenommen, dass eine Ausgabe (sprich ein Programm) existiert das die Spezifikationen erfüllt. Daraufhin wird ein konstruktiver Beweis vom Automatischen Beweiser verlangt. Die Struktur des Programms ist somit durch den Beweis festgelegt. Wenn z.B. Induktion in dem Beweis verwendet wurde, so findet sich im Programm Rekursion oder Schleifen. Das entstandende Programm ist korrekt, in diesem Kontext, denn der Beweis hängt von den Axiomen der verwendeten Theorie ab. Die verwendete Implementierung von SNARK verwendet die Auflösungs- und die Paramodulationsregel um Formeln der Prädikaten-Logik erster Ordnung mit Gleichheit verarbeiten zu können. Er ist in COMMON LISP programmiert. Es ist möglich die Beweise auf konstruktive zu beschränken, so dass es möglich ist Programme zu extrahieren. Um die Generierung der Programme performanter zu machen wurde ausgenutzt, dass SNARK so genanntes "recursive-path-ordering" unterstützt. Diese Technik ist abgeschlossen für Prädikaten-Logik erster Ordnung mit Gleichheit, d.h. wenn ein Beweis existiert, kann dieser gefunden werden unabhängig von der verwendeten Ordnung. Jedoch mag es sein, dass innerhalb einer gegebenen Zeit mit bestimmten Ressourcen der Beweis nur mit einer speziellen Ordnung gefunden werden kann. Denn die Technik ist eine starke Optimierung der Performance von SNARK.
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung Nächster Gliederungspunkt Technik "recursive-path-ordering" | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Beispielanwendung Amphion | ||||
| ||||
| ||||
| ||||
| ||||
 | Untergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
