La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

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

157 pages
GraphTransformationSystemsinConstraintHandlingRules:ImprovedMethodsforProgramAnalysisDISSERTATIONzurErlangungdesDoktorgradesDr.rer.nat.derFakultätfürIngenieurwissenschaftenundInformatikderUniversitätUlmFrankRaiserausFüssenUniversitätUlmFakultätfürIngenieurwissenschaftenundInformatikInstitutfürProgrammiermethodikundCompilerbauInstitutsdirektor: Prof.Dr.HelmuthPartschNovember2010Amtierender Dekan: Prof. Dr.-Ing. Klaus Dietmayer1. 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 2010AcknowledgmentsAs with any work of this size and scope, it only came to existence due to a seemingly randomchain of events and the more or less direct influence of other people. At this point, I wouldlike to take some time (or rather space) to express my gratitudes to those who are responsiblefor 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 forhim, I came to know about the intricacies involved in academic research, of which only veryfewarerelatedtoactualscientifictopics. Astheyearsprogressed, hesupportedmeinlearningthe ropes, which proved to be just as important for a doctoral career as the scientific contentitself.
Voir plus Voir moins

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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
7.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
7.2 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
7.3 Program Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
IIIA Complete and Terminating Operational Semantics for Constraint Han-
dling Rules 31
8 Equivalence-based Operational Semantics . . . . . . . . . . . . . . . . . . . . 32
8.1 State Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8.2 State Transition System . . . . . . . . . . . . . . . . . . . . . . . . . . 41
9 Constraint Handling Rules with Persistent Constraints . . . . . . . . . . . . . 44
9.1 State Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
9.2 State Transition System . . . . . . . . . . . . . . . . . . . . . . . . . . 47
10 Merge Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
10.1 Properties of the Merge Operator . . . . . . . . . . . . . . . . . . . . . 50
v10.2 Partial Order on States . . . . . . . . . . . . . . . . . . . . . . . . . . 53
11 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
11.1 Formulations of State Transition System . . . . . . . . . . . . . . . . . 54
11.2 Range-Restrictedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
11.3 Termination Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
11.4 Expressivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
11.5 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
12 Related and Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
IVImproved Program Analysis Methods 75
13 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
13.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
13.2 Advantages and Disadvantages . . . . . . . . . . . . . . . . . . . . . . 76
13.3 Implications for Program Analysis . . . . . . . . . . . . . . . . . . . . 78
14 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
14.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
14.2 Invariant-based Confluence . . . . . . . . . . . . . . . . . . . . . . . . 84
15 Program Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
15.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
15.2 Reduced Restrictions for Program Equivalence . . . . . . . . . . . . . 91
15.3 Invariant-based Program Equivalence . . . . . . . . . . . . . . . . . . 93
16 Related and Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
V Embedding Graph Transformation Systems in Constraint Handling Rules 99
17 Encoding of Graph Transformation Systems . . . . . . . . . . . . . . . . . . . 99
17.1 Encoding Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
17.2 Encoding Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
18 Properties of Encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
18.1 Graph States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
18.2 Partial Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
18.3 Soundness and Completeness . . . . . . . . . . . . . . . . . . . . . . . 109
19 Confluence Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
19.1 Correspondence of Critical Pairs . . . . . . . . . . . . . . . . . . . . . 114
19.2 Deciding Confluence via Embedding . . . . . . . . . . . . . . . . . . . 115
19.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
20 Program Equivalence Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 123
20.1 Redundant Rule Removal . . . . . . . . . . . . . . . . . . . . . . . . . 124
21 Related and Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
VIConclusion 127
22 Equivalence-based operational semantics . . . . . . . . . . . . . . . . . . . . . 127
23 Program Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
24 Encoding of Graph Transformation Systems . . . . . . . . . . . . . . . . . . . 128
Bibliography 131
Index 141
viList of Tables
II.1 State Transition System ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10va
II.2 State T ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12t
II.3 State Transition System ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14p
III.1 Comparison of Different State Equivalence Definitions . . . . . . . . . . . . . 35
III.2 State Transition System ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42e
III.3 State T ω with Equivalence Classes . . . . . . . . . . . . . . 44e
III.4 State Transition System ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48!
III.5 Different Formulations of the Operational Semantics ω over Σ . . . . . . . . 56e e
III.6t Form of the Optics ω over Σ /≡ . . . . . . 56e e e
III.7 Different Formulations of the Operational Semantics ω over Σ . . . . . . . . 57! !
III.8t Form of the Operational Semantics ω over Σ/≡ . . . . . . 58! ! !
viiviii

Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin