Description logic based reasoning on programming languages

Abstract

Imperative Programmiersprachen sind in praktisch allen technologischen Bereichen verbreitet, wobei Programme verschiedene Arten von Berechnungen spezifizieren. Für viele praktische Zwecke ist die automatisierte Analyse semantischer Eigenschaften von Programmen, wie die Terminierung und Äquivalenz, nützlich. Wir stellen ein neues Vorgehen zur automatisierten semantischen Analyse von Programmen bereit durch die Kodierung ihres Verhaltens in die formale Logik. Wir betrachten einige syntaktisch einfache, imperative Programmiersprachen, und wir kodieren Programme dieser Sprachen in Ausdrücke der Beschreibungslogik ALC(D), für einen bestimmten Bereich D. Wir machen das in einer Weise, in der Modelle dieser Kodierungen den Durchführungen der Programme entsprechen. Mit anderen Worten, wir weisen imperativen Programmen eine modelltheoretische Semantik zu. Diese Kodierung ermöglicht es semantische Eigenschaften von Programmen (vor allem Terminierung und Äquivalenz) in der Sprache der formalen Logik auszudrücken. Auf diese Weise reduzieren wir das Schlussfolgern diverser semantischer Eigenschaften von Programmen zu Reasoning-Verfahren der Beschreibungslogik. In praktischer Hinsicht führt dieses Vorgehen direkt zu Algorithmen für das automatisierte Schlussfolgern für einige Fragmente der Programmiersprachen (d.h. Zyklusfreie Programme oder Programme beschränkt auf endliche numerische Bereiche). In theoretischer Hinsicht ermöglicht das Vorgehen weitere, weniger eingeschränkte Fragmente der Programmiersprachen zu identifizieren, wofür einige Aufgaben des Schlussfolgerns entscheidbar sind. Wir identifizieren Eins solcher Fragmente, welches auf endliche Aufteilungen des Zustandsraums basiert, und wir illustrieren, welche Klasse von Programmen zu diesem Fragment gehört.<br />

Imperative programming languages are ubiquitous in virtually all fields of technology, with programs specifying all sorts of computational behavior. For many practical reasons, an automated analysis of semantic properties of programs, such as termination and equivalence, is desirable. We provide a new approach to the automated semantic analysis of programs by encoding their behavior into formal logic. We consider a few syntactically simple imperative programming languages, and we encode programs of these languages into expressions of the description logic ALC(D) for a particular domain D. We do this in such a way that models of these encodings correspond to executions of the source programs. In other words, essentially, we assign a model-theoretic semantics to imperative programs. This encoding makes it possible to express semantic properties of programs (most notably termination and equivalence) in the formal logic language. Effectively, in this fashion, we reduce reasoning problems defined on the programs to description logic reasoning.<br />Practically, this directly results in algorithms to perform automated reasoning on a number of restricted fragments of the programming languages (i.e. loop-free programs, or programs restricted to a finite numerical domain). Theoretically, our approach makes it possible to identify further, less restricted fragments of the programming languages for which certain reasoning tasks are decidable. We identify one such fragment, based on finite partitionings of the state space, and illustrate what class of programs belongs to this fragment.