Praktische Probleme bei der Konstruktion von Software zur automatisierten Terminierungsanalyse
Loading...
Date
2014-09-29
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Alternative Title(s)
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.
Description
Table of contents
Keywords
Terminierungsanalyse imperativer Programmiersprachen, Transformation imperativer Programme zu funktionalen Programmen, Umsortieren von Anweisungen, Semantische Äquivalenz von Permutationen von Anweisungen, Operationelle Semantik von Ein- und Ausgabeanweisungen