A Set-Based Calculus and its Implementation
vorgelegt von Diplom-Informatiker
Wolfgang Grieskamp
aus Essen
Am Fachbereich 13, Informatik,
der Technischen Universit¨
at Berlin
zur Erlangung des akademischen Grades
Doktor der Ingenieurwissenschaften
– Dr.-Ing. –
genehmigte Dissertation
Promotionsausschuß:
Vorsitzender : Prof. Dr. G¨
unter Hommel
Berichter : Prof. Dr. Peter Pepper
Berichter : Prof. Dr. Stefan J¨
ahnichen
Tag der wissenschaftlichen Aussprache: 26.11.1999
Berlin 1999
D 83
Meinen Eltern
Zusammenfassung
Diese Arbeit untersucht die Fundierung und Implementierung eines Berechnungsmodells
f¨ur mengenbasierte Computersprachen. Es wird das
Z-Kalk¨ul eingef¨uhrt, eine mini-
male mengenbasierte Ausdruckssprache, verwandt mit dem
-Kalk¨ul, das Anwendungs-
sprachen wie die Spezifikationssprache Z oder funktional-logische Programmiersprachen
komplett und nat¨urlich einbetten kann. Syntax,Semantik und Gleichungstheorie von
Z
werden definiert. Mehrere Berechnungsmodelle werden entwickelt. Durch gezielte An-
wendung der Gleichungstheorie ergibt sich eine Narrowingsemantik, die durch lokale
Modifikation der Redexauswahl nicht-strikt oder strikt ausf¨allt, und insbesondere interes-
sant f¨ur interpretative “on-line” Auswertung ist, da sie auf symbolischer Termersetzung
basiert. Das zentrale Berechnungsmodell aber basiert auf einer nat¨
urlichen Semantik, die
durch ihren operationalen Charakter das Design kompilierter “off-line” Auswertung vor-
bereitet, und das Berechnungsreferenzmodell von
Zfestlegt. Dieses Modell kombiniert
funktionale Reduktion und nebenl¨aufige Resolution, und definiert eine klare Trennung
zwischen der (deterministischen, funktionalen) Konstruktion von Mengen und der (nicht-
deterministischem, logischen) Dekonstruktion. Da Mengen sowohl extensional als auch
intensional dargestellt werden k¨onnen, ist das Modell von h¨oherer Ordnung.
Die Implementierung erfolgt in Form einer abstrakten Maschine, der ZAM, welche
auf der Technik nebenl¨aufiger Resolutionsagenten basiert. Die Maschine realisiert eine
effiziente Tiefensuche ¨uber die Verwaltung von Auswahlpunkten und Modifikationspro-
tokollen. Durch ein Priorit¨atenmodell in der nebenl¨aufigen Ausf¨uhrung werden nichtde-
terministische Berechnungen dynamisch verz¨ogert und deterministische propagiert. Die
ZAM ist als Stackmaschine vollst¨andig in Z spezifiert, und wird in der Implementierung
in C++ zu einer Registermaschine verfeinert, welche persistente Register verwendet, um
den Aufwand der Protokollierung von Modifikation zu minimieren.
Die Anwendung der vorgestellten Konzepte erfolgt im Rahmen des ZeTa Systems,
im BMBF Projekt ESPRESS entwickelt, das verschiedenartige Notationen und Werkzeuge
auf der semantischen Grundlage von Z integriert. Der ZaP ¨
Ubersetzer, Bestandteil des
ZeTa Systems, realisiert mit Hilfe des
Z-Kalk¨uls die Ausf¨uhrung von Z Modellen, und
wurde beispielsweise in ESPRESS f¨ur die Automatisierung von Softwaretests eingesetzt.
Die Definition von
Z, der Berechnungsmodelle, der abstrakten Maschine und der
¨
Ubersetzung von
Zin Maschinencode ist vollst¨andig in der Spezifikationssprache Z ge-
geben (mit kleineren syntaktischen Erweiterungen), und daher syntax- und typgepr¨uft.
Insofern ist diese Arbeit auch eine Fallstudie der Anwendbarkeit von Z f¨ur anspruchsvol-
le Probleme der Metamodellierung.
Preface
In response to those who thought that Cantor’s theory of sets might be destroyed by the
well-known paradoxes discovered at the beginning of this century, Hilbert once spoke
about the “paradise created by Cantor from which nobody shall ever expel us” (quoted
in Vaught [1995]). On the level of non-constructive calculi, the beauty of the set-based
approach has been recognized in computer science in the formal notation Z [Spivey, 1992;
Toyn, 1998], developed in the eighties and semantically based on Zermelo-Fraenkli set
theory, which solves the paradoxes of classical set theory. In recent years, a growing
number of authors haveadvocated the useof sets in declarativeprogramming and program
analysis.
In this thesis, I use the set-based approach as the basis for a novel, small intermediate
calculus, which allows to naturally embed concepts from higher-order functional, logic
and concurrent constraint programming, as well as set-based specification languages such
as Z. I define the syntax and semanticsof the calculus, analyze its equational theory, inves-
tigate several computation models, provide an abstract machine that implements a model,
and define a compilation from the calculus to the machine. The power of the calculus
and its implementation allows an unorthodox approach to the integration of higher-order
functional and constraint logic programming.
The present thesis, written between January and September 1999, grew out of my ac-
tivities in the application oriented research project ESPRESS (1995-1998), which was con-
cerned with methods and tools for the specification of safety-critical embedded systems
[B¨ussow et al., 1996; B¨ussow and Grieskamp, 1997; B¨ussow et al., 1997a; Grieskamp
et al., 1998; B¨ussow et al., 1998; B¨ussowand Grieskamp, 1999]. One goal in the ESPRESS
context was to provide a tool to execute Z specifications, for the purpose of evaluating
test data and animating requirements specification of embedded systems based on Z. The
development of a compiler for Z was influenced by my earlier experiences with the im-
plementation of the algebraic-functional language Opal [Schulte and Grieskamp, 1992;
Hartel et al., 1996; Didrich et al., 1994; Frauenstein et al., 1996a,b; Didrich et al., 1998],
which strongly suggested basing such a compiler on a small intermediate language in
the style of the
-calculus. This led to a first design of the calculus presented in this
thesis, called
Zbecause of its original purpose for abstracting from the diversity of the
Z notation. This first version was used as an intermediate language in the experimental
compiler ZaP, which is part of the Z-based tool-integration environment ZeTa [B¨ussow
and Grieskamp, 1999], developed under the supervision of the author in ESPRESS.ZaP
has proved to be a feasible tool, in particular for the evaluation of test data, and it is being
used for this purpose in several projects conducted in cooperation with Daimler-Chrysler,
FT3/SM, Berlin. The work presented here consolidates and refines the technology of ZaP
on the basis of these experiences. On the one hand, it closes the gap between the exper-
Loading more pages...