Set based failure diagnosis for concurrent constraint programming [Elektronische Ressource] / von Martin Ludwig Müller

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2004
• Nombre de lectures: 20
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Set-based Failure Diagnosis for
Concurrent Constraint Programming
Dissertation
zur Erlangung des Grades
Doktor der Ingenieurwissenschaften (Dr.-Ing.)
der Technischen Fakultat¨
der Universitat¨ des Saarlandes
von
Martin Ludwig Muller¨
Saarbruck¨ en
Mai 1998Martin Muller¨
Forschungsbereich Programmiersysteme
Universit¨at des Saarlandes, 66041 Saarbr¨ucken, Germany
[e-mail]
http://www.ps.uni-sb.de/˜mmueller/
Vorsitzender: Prof. Dr. Harald Ganzinger
Erstgutachter: Prof. Dr. Gert Smolka
Zweitgutachter: Priv.-Doz. Dr. Andreas Podelski
Tag des Kolloquiums: 22. Juli 1998Kurze Zusammenfassung
Oz ist eine anwendungsnahe Programmiersprache, deren Grundlage eine Erweiterung
des Modells nebenl¨aufiger Constraintprogrammierung um Prozeduren h¨oherer Stufe
und Zustand ist. Oz ist eine Sprache mit dynamischer Typ¨uberpr¨ufung wie Prolog,
Scheme oder Smalltalk. Wir untersuchen zwei Ans¨atze, statische Typ¨uberpr¨ufung f¨ur
Oz zu erm¨oglichen: Mengenbasierte Fehlerdiagnose und Starke Typisierung. Wir
definieren ein neues System von Mengenconstraints ¨uber Featureb¨aumen, das f¨ur
die Analyse von Recordstrukturen geeignet ist, und wir untersuchen das Erf¨ullbar-
keits-, das Leerheits- und das Subsumtionsproblem f¨ur dieses Constraintsystem. Wir
pr¨asentieren eine mengenbasierte Diagnose f¨ur Constraint-Logikprogrammierung und
f¨ur nebenl¨aufige Constraintprogrammierung als Teilsprachen von Oz, und wir be-
weisen, daß diese unvermeidliche Laufzeitfehler erkennt. Wir schlagen auch eine
mengenbasierte Analyse f¨ur eine gr¨ossere Teilsprache von Oz vor. Komplement¨ar
dazu definieren wir eine Oz-artige Sprache genannt Plain, die ein expressives starkes
Typsystem erlaubt. Wir stellen ein solches Typsystem vor und beweisen seine Korrekt-
heit.iiZusammenfassung
Das Modell nebenl¨aufiger Constraintprogrammierung (Concurrent Constraint Model,
CC) stellt eine einfache und doch m¨achtige Grundlage f¨ur problemnahe nebenl¨aufige
Programmiersprachen dar. Die Expressivit¨at des CC-Modells wird erheblich erwei-
tert durch das Oz Programmiermodell (OPM), welches der Programmiersprache Oz
zugrunde liegt. Oz subumiert etablierte Programmierparadigmen wie das der funk-
tionalen, der objekt-orientierten, oder der constraintbasierten Programmierung. Ins-
besondere verf¨ugt Oz ¨uber Ausdrucksmittel zur Programmierung von constraintba-
sierten Inferenzverfahren, die ¨uber alle aus der Constraint-Logikprogrammierung be-
kannten hinaus gehen.
Oz ist eine Sprache mit dynamischer Typ¨uberpr¨ufung wie Prolog, Scheme oder Small-
talk. Das heißt zum einen, daß Oz eine typsichere Sprache ist, die die typkorrekte Ver-
wendung von primitive Operationen garantiert; es bedeutet andererseits, daß Oz keine
statische Typ¨uberpr¨ufung durchf¨uhrt. Dynamische Typ¨uberpr¨ufung ist von Vorteil
f¨ur die Einfachheit und Flexibilit¨at einer Programmiersprache, aber es erschwert die
Fehlersuche in Programmen. In dieser Arbeit untersuchen wir zwei Ans¨atze, statische
Typ¨uberpr¨ufung f¨ur Oz zu erm¨oglichen: Mengenbasierte Fehlerdiagnose und Starke
Typisierung.
Mengenbasierte Fehlerdiagnose ist ein Programmanalyseverfahren, dessen Ziel es ist,
¨Programmierfehler schon zur Ubersetzungszeit zu erkennen. Das Verfahren wird
als mengenbasiert bezeichnet, weil es eine Klasse pr¨adikatenlogischer Formeln ver-
wendet, die ¨uber Mengen von B¨aumen interpretiert werden (sogenannte Mengencon-
straints). Der Entwurf einer mengenbasierten Programmanalyse verl¨auft in drei Schrit-
ten: Zun¨achst definiert man eine Klasse von Mengenconstraints, die f¨ur die gegebene
Programmiersprache und das Analyseproblem angemessen ist. Dann definiert man
eine Abbildung von Programmen in diese Mengenconstraints und beweist, daß die
Abbildung bestimmte Laufzeiteigenschaften des Programms erh¨alt. Schließlich ent-
wickelt man Algorithmen, um die verwendeten Constraints zu l¨osen.
Wir definieren ein neues System von Mengenconstraints ¨uber Featureb¨aumen. Dieses
Constraintsystem ist durch die Analyse von Records motiviert, die in Oz eine zentrale
Rolle spielen, und die in Oz durch Gleichheitsconstraints ¨uber Featureb¨aumen in Oz
integriert sind. Wir untersuchen das Erf¨ullbarkeits-, das Leerheits- und das Subsum-
tionsproblem f¨ur Mengenconstraints ¨uber Featureb¨aumen und pr¨asentieren eine Reihe
von Algorithmen und Komplexit¨atsergebnissen. Mengenconstraints ¨uber Featureb¨au-
men sind von unabh¨angigem Interesse, ¨uber ihre Verwendung in der Programmanalyse
hinaus und insbesondere im Vergleich mit bekannten Mengenconstraintsystemen.
Wir geben eine mengenbasierte Diagnose an f¨ur Constraint-Logikprogrammierung
und nebenl¨aufige Constraintprogramming als Fragmente erster Stufe von Oz. Als
Korrektheitsbeweis f¨ur unsere Diagnose zeigen wir, daß sie nur Programme zur¨uck-
weist, die einen unvermeidlichen Laufzeitfehler enthalten. F¨ur eine gr¨ossere Teil-sprache von Oz, die insbesondere Prozeduren h¨oherer Stufe mit einschließt, geben wir
eine Analyse an und illustrieren sie anhand von Beispielen. Das interessante Korrekt-
heitsproblem f¨ur diese Analyse lassen wir offen. Durch die Prozeduren h¨oherer Stufe
wird das Korrektheitsproblem wesentlich schwieriger und die Beweistechniken f¨ur den
Fall erster Stufe sind nicht mehr anwendbar.
Komplement¨ar zu der mengenbasierten Diagnose untersuchen wir den Entwurf eines
streng statischen Typsystems f¨ur Teilsprachen von Oz. Wir definieren Plain und wir
zeigen, daß ein expressives starkes Typsystem m¨oglich ist f¨ur eine Sprache, die we-
sentliche Elemente von Oz kombiniert: darunter Prozeduren h¨oherer Stufe, Logische
Variablen und partiell determinierte Datenstrukturen, Zellen und Records. Anderer-
seits heben wir einige Einschr¨ankungen von Plain gegen¨uber Oz hervor. Plains Typ-
system unterst¨utzt Recordtypen, Untertypen, polymorphe Typen h¨oherer Stufe, Modi
und Modus-Polymorphismus. Wir beweisen die Korrektheit unseres Typsystems mit
Hilfe eines Typerhaltungssatzes (subject reduction).
ivShort Abstract
Oz is a recent high-level programming language, based on an extension of the concur-
rent constraint model by higher-order procedures and state. Oz is a dynamically typed
language like Prolog, Scheme, or Smalltalk. We investigate two approaches of making
static type analysis available for Oz: Set-based failure diagnosis and strong typing.
We define a new system of set constraints over feature trees that is appropriate for the
analysis of record structures, and we investigate its satisfiability, emptiness, and en-
tailment problem. We present a set-based diagnosis for constraint logic programming
and concurrent constraint programming as first-order fragments of Oz, and we prove
that it correctly detects inevitable run-time errors. We also propose an analysis for a
larger sublanguage of Oz. Complementarily, we define an Oz-style language called
Plain that allows an expressive strong type system. We present such a type system and
prove its soundness.viAbstract
Concurrent constraint (CC) programming is a simple and powerful high-level model
for concurrent programming. The expressiveness of the CC model has been conside-
rably extended by the Oz Programming Model (OPM) which is realised in the pro-
gramming language Oz. Oz subsumes well-established programming paradigms such
as higher-order functional and object-oriented programming, and it supports problem
solving facilities beyond those known from constraint logic programming.
Oz is a dynamically typed language like Prolog, Scheme, or Smalltalk. This means that
Oz is a type safe language that guarantees type-correctness of primitive operations, but
that it lacks static (compile-time) type checking. This is advantageous for simplicity
and flexibility of the language but it complicates the debugging of programs. In this
thesis we investigate two approaches of making static type checking available for Oz:
Set-based failure diagnosis and strong typing. failure is a method for program analysis with the goal to detect
programming errors at compile-time. The method is called set-based because it em-
ploys set constraints, a class of predicate logic formulas interpreted over sets of trees.
The design of a set-based program analysis involves the following steps. First, one
defines a class of set constraints that is appropriate for the given language and the ana-
lysis problem. Second, one defines a mapping from programs to set constraints and
proves that this mapping preserves certain run-time properties of the programs. Third,
one provides algorithms to solve the constraints.
We define a new system of set constraints over feature trees. This constraint system
is motivated by the analysis of records, since Oz incorporates records as a central data
structure through equality constraints over feature trees. We study the satisfiability,
emptiness, and entailment problems for set constraints over feature trees and provide a
number of a