Automatische Terminierungsanalyse von imperativen Programmen   

 

Matthias Sonderman

 

 

Abstract:

 

Wir stellen ein Rahmenwerk vor, das eine Übersetzung eines
imperativen Programms bezüglich eines gegebenen Startzustands
in ein Termersetzungssystem ermöglicht, um über diesen Weg
die Terminierung des Programms zu beweisen. Als zugrunde
liegende Sprache wird eine Teilmenge der Programmiersprache
Java verwendet, die wir durch Transformationen auf eine
kleine Teilmenge von Syntaxkonstrukten einschränken können.

Darauf aufbauend konstruieren wir zu jeder Methode einen
Kontrollflussgraph, der die Verkettung der im Rumpf
auftretenden Anweisungen repräsentiert. Anhand dieses
Graphen führen wir eine Live-Variable-Analyse durch, die zu
jeder Anweisung eine Menge von Variablen berechnet, die im
weiteren Programmverlauf verwendet werden. Durch sie ist es
möglich, die Stelligkeit der Funktionssymbole im Termer-
setzungssystem erheblich zu reduzieren.

Basierend auf dem Kontrollflussgraph stellen wir eine
symbolische Auswertung vor, deren Ergebnis der Finite-
Interpretation-Graph ist, dessen Pfade alle möglichen
Auswertungen enthalten. Die Zyklen des Graphen bilden
die Grundlage der DP-Problem-Generierung. Es wird bewiesen,
dass in einem der DP-Probleme eine unendliche DP-Kette
konstruiert werden kann, falls im Originalprogramm eine
unendliche Auswertung bezüglich des gegebenen Startzustands
existiert. Somit kann insgesamt das Dependency-Pair-
Framework zur Terminierungsanalyse imperativer Programme
verwendet werden.