Praktische Probleme bei der Konstruktion von Software zur automatisierten Terminierungsanalyse

Abstract

Die Arbeit beschäftigt sich mit den Einsatzmöglichkeiten bereits bestehender automatisierter Verfahren zur Terminierungsanalyse für die Klasse der praktische relevanten, imperativen Programmiersprachen.

Die automatisierte Terminierungsanalyse ist für Termersetzungssysteme besonders gut untersucht. Eine Anwendung der resultierenden Methoden ist für deklarative Programmiersprachen mit beachtlichem Erfolg möglich, während sich eine Anwendung auf imperative Sprachen schwieriger gestaltet.

Jedoch können durch Ausnutzung der großen Ausdrucksstärke funktionaler Programmiersprachen imperative Programme durch funktionale Programme simulieren. Es wird untersucht, inwiefern die resultierenden funktionalen Programme der Terminierungsanalyse mit Termersetzungsmethoden zugänglich sind. Es werden verschiedene Probleme gezeigt, die durch Anwendung bestimmter Programmtransformationen gelöst werden können, sodass arithmetische Teilprogramme einer Terminierungsanalyse zugänglich werden. Es wird auch gezeigt, dass dieser Ansatz nicht zur Analyse von Programmen, die dynamisch Speicher allozieren genutzt werden kann.

Ein weiteres Problem bei der Analyse praktisch relevanter, imperativer Sprachen aus der Praxis stellen Ein- und Ausgabeanweisungen dar. Da diese den bestehenden Verfahren unzugänglich sind, sind im Allgemeinen Transformationen notwendig, um zumindest Teilprogramme zu analysieren. Es wird daher eine formale Semantik für eine imperative Sprache mit Ein- und Ausgabeanweisung eingeführt. Auf dieser Grundlage wird ein Kriterium entwickelt, welches erlaubt, die semantische Äquivalenz einer Permutation einer Anweisungsfolge nachzuweisen.