Graph transformation systems in Constraint Handling Rules [Elektronische Ressource] : improved methods for program analysis / Frank Raiser

Sujets

• Informatik

Informations

• Publié par: universitat_ulm
• Publié le: 01 janvier 2010
• Nombre de lectures: 25
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

GraphTransformationSystems
inConstraintHandlingRules:
ImprovedMethodsforProgramAnalysis
DISSERTATION
zurErlangungdesDoktorgradesDr.rer.nat.
derFakultätfürIngenieurwissenschaftenundInformatik
derUniversitätUlm
FrankRaiser
ausFüssen
UniversitätUlm
FakultätfürIngenieurwissenschaftenundInformatik
InstitutfürProgrammiermethodikundCompilerbau
Institutsdirektor: Prof.Dr.HelmuthPartsch
November2010Amtierender Dekan: Prof. Dr.-Ing. Klaus Dietmayer
1. Gutachter: Prof. Dr. Dr. Thom Frühwirth (Ulm University)
2. Gutachter: Prof. Dr. Enno Ohlebusch (Ulm University)
3. Gutachter: Prof. Dr. Slim Abdennadher (German University in Cairo)
Tag der Promotion: 09. November 2010Acknowledgments
As with any work of this size and scope, it only came to existence due to a seemingly random
chain of events and the more or less direct influence of other people. At this point, I would
like to take some time (or rather space) to express my gratitudes to those who are responsible
for this work coming to fruition, probably as much as myself, if not more so.
First and foremost, I want to thank my supervisor Thom Frühwirth. Through working for
him, I came to know about the intricacies involved in academic research, of which only very
fewarerelatedtoactualscientifictopics. Astheyearsprogressed, hesupportedmeinlearning
the ropes, which proved to be just as important for a doctoral career as the scientific content
itself. Last, but not least, he supported my urge to travel around the world and visit different
places, especially when there were suitable conferences nearby.
Deepest thanks also go to Marc Meister, who accompanied my journey in the early years and
in countless hours of discussions revealed not only tremendous knowledge to me, but also his
artistic talent – for his words continuously painted pictures of my future, ranging from the
bleak to the bright. Looking back at these pictures from where I stand now, they served me
well in avoiding those dark pitfalls.
I also want to thank the whole institute of Software Engineering and Compiler Construction,
which became my second home for all these years. In particular, its director Helmut Partsch,
who despite his many duties always remained approachable and helpful. And I want to
thank my co-workers Ingmar Baetge, Hariolf Betz, Armin Bolz, Marcel Dausend, Ralf Gerlich,
Dominik Gessenharter, Walter Guttmann, Carolin Hürster, Jens Kohlmeyer, Sandra Mann,
Alexander Raschke, Stefan Sarstedt, and Matthias Schneiderhan for providing a fantastic
atmosphere. Although they all perform research in other areas and we spared no excuse to
light-heartedly ridicule each other’s, we all became good friends and shared much more than
just the burden of work. In my few years here, the institute also saw three secretaries –
Claudia Hammer, Ulrike Seiter, and Eva Englert – to whom not only I am grateful, as their
work gave all of us more time to persue our doctoral studies.
Further thanks go to the many scientific colleagues I have met all around the world for the
numerous fruitful discussions. I’d like to especially thank Jon Sneyers and Peter van Weert
with whom it was a pleasure to organize our various meetings and Slim Abdennadher for the
wonderful time in Egypt.
Finally, I am grateful to all my friends, and in particular Martina Reng, for supporting me
in any way possible during these often chaotic years. Their presence and friendship has truly
enriched my life.
In the end, let me return to the beginning and thank my parents who have successfully
iprepared me for this journey and unfailingly believed in me. Due to my father’s untimely
death he could no longer witness the completion of this work and because his life was as far
from its subject as one could imagine, I believe it to be even more appropriate to dedicate
this thesis to him.
to my father
iiSummary
In recent years, the importance of rule- and logic-based technologies steadily intensified, and
nowadays, we witness their increased industrial adoption. Constraint Handling Rules (CHR)
is one of these formalisms and has established itself as an active research topic during the last
two decades. In contrast to other rule-based approaches, CHR is both, a theoretical formalism
related to first-order and linear-logic, and a practical rule-based programming language.
Research on CHR revealed, that it is a remarkable declarative language. For example, al-
though it is logic-based, every algorithm can be implemented in CHR in optimal time and
space complexity. Furthermore, its execution efficiency is outstanding, in that it consistently
outperforms other state-of-the-art production rule systems.
Other rule- and logic-based approaches, like term rewriting, logical algorithms, or petri nets,
have been successfully embedded in CHR. For this reason, it is considered a candidate for
a lingua-franca of such approaches, which provides the basis for our work. We investigate
CHR’s suitability for this purpose exemplarily, by considering an embedding of graph trans-
formation systems (GTSs) in CHR, which helps us in identifying points of improvements for
strengthening the lingua-franca argument further.
In particular, we identify shortcomings of current formulations of the operational semantics
of CHR. We present a novel formulation in order to alleviate these, which is founded on
an equivalence relation over CHR states. It justifies the perspective on CHR as a rule-
based rewriting system of equivalence classes, which abstracts over infinitely many possible
syntactic variations of a CHR state. Furthermore, the resulting transition system is suitable
for teaching CHR, as it is given by a single intuitive inference rule. Overall, this equivalence-
based operational semantics provides a powerful formal analysis tool for CHR, which can
significantly reduce proof complexity.
The lingua-franca argument implies a potential for cross-fertilization of research. Hence, we
revisit program analysis methods available in the CHR literature from the point of view of our
equivalence-based operational semantics. We extend existing program analysis methods, in
particular for confluence and program equivalence, to support invariants. The tra-
ditional methods often fail for states that are irrelevant, given the assumptions made by the
programs’ developers. Our extended methods apply an invariant to make these implicit as-
sumptions explicitly available during analysis, hence, effectively eliminating irrelevant states.
The resulting methods are applicable to strictly larger classes of CHR programs and provide
more promising approaches towards analyzing more complex programs.
Wethenreturntotheabovelingua-francaargument, byreconsideringourembeddingofgraph
transformation systems in CHR under the equivalence-based operational semantics. This
iiiconfirms the suitability of our improvements to the operational semantics, by for example,
revealing a closer correspondence between graph isomorphism and state equivalence in CHR.
Finally, we put the research cross-fertilization argument of a lingua-franca to the test, when
comparing program analysis methods in both systems. Confluence is particularly interesting,
because its decidability differs for GTSs and CHR programs. We find that the adapted
CHR confluence test, when applied to a GTS embedded in CHR, corresponds to a sufficient
criterion for confluence of the GTS. Similarly, we introduce program equivalence for GTSs
with a sufficient criterion based on the CHR program equivalence test.
In summary, our work provides novel program analysis methods that are capable of examining
programs under the environment assumed by their developers. We exemplarily applied the
lingua-franca argument to GTSs, which yielded relevant insights into confluence analysis of
CHR programs and a program equivalence test for GTSs. In conclusion, our work provides
a stronger foundation for CHR as a lingua-franca, based on the more versatile and intuitive
equivalence-based operational semantics.
ivContents
Table of Contents vi
List of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii
List of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix
List of Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xi
I Introduction 1
1 Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2 Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
4 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
II Background 7
5 Constraint Handling Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
5.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
5.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
5.3 Relation to Other Formalisms . . . . . . . . . . . . . . . . . . . . . . . 17
6 Graph Transformation Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 19
6.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
6.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
7 Program Analysis . . . . . . . . . . . . . . . . . . . . .