No label defined (Q4519871)

Einführung: Diese Arbeit entstand im Rahmen eines Forschungsprojektes innerhalb der ``Zentralabteilung Technik'' der Siemens AG. Im Rahmen des Werkzeugs zur statischen Analyse von Prologprogrammen PAN, das die Überprüfung der korrekten Typisierung bezüglich eines eigens entwickelten Typsystems mit Inklusions- und parametrischem Polymorphismus, den Nachweis der Terminierung, sowie die Analyse gewisser Konsistenz- und Vollständigkeitseigenschaften von Prologprogrammen erlaubte, sollte eine Methode zur Verifikation einfacher Programmeigenschaften gefunden werden, die eine gute Hilfestellung bei der Aufdeckung von Fehlern ermöglichte. Die Arbeit stellt ein Semientscheidungsverfahren für die Gültigkeit einfacher Programmeigenschaften dar. Das Verfahren terminiert immer bei Eingabe falscher Aussagen und liefert dann ein Gegenbeispiel. Das Verfahren beruht auf impliziten Induktionsmethoden. Durch die Unterstützung eines entsprechenden Typsystems lässt sich das Verfahren zur Verifikation von Programmeigenschaften im Rahmen von PAN nutzen. Da die Verwendung der Ergebnisse der im Rahmen von PAN gemachten Terminierungsanalyse an die Stelle der üblichen Termordnungen tritt, ist das Verfahren einfacher und vielseitiger anwendbar als bisher bekannte Verfahren.