Loading…
Thumbnail Image

A set-based calculus and its implementation

Grieskamp, Wolfgang

Diese Arbeit untersucht die Fundierung und Implementierung von Berechnungsmodellen für mengenbasierte Computersprachen. Es wird der micro-Z-Kalkül eingeführt, eine minimale mengenbasierte Sprache, welcher Anwendungssprachen wie die Spezifikationssprache Z oder funktional-logische Programmiersprachen komplett und natürlich einbetten kann. Syntax, Semantik und Gleichungstheorie von MZ werden definiert. Mehrere Berechnungsmodelle werden entwickelt. Das Referenzberechnungsmodell, mit der Technik der natürlicher Semantik definiert, kombiniert funktionale Reduktion und nebenläufige Resolution, und bereitet die Implementierung durch eine abstrakte Maschine vor, welche auf nebenläufigen Resolutionsagenten basiert. Die Resultate der Arbeit sind eingebettet im Kontext des BMBF Forschungsprojekts ESPRESS, und wurden z.B. für die Automatisierung von Softwaretests eingesetzt. Die formalen Anteile dieser Arbeit sind vollständig in syntax- und typgeprüften Z gegeben, so dass die Arbeit auch eine Fallstudie der Anwendbarkeit von Z für anspruchsvolle Probleme der Metamodellierung darstellt.
This thesis is concerned with the foundation and implementation of a computation models for set-based computer languages. It introduces the micro-Z calculus, a small set-based expression language, which is able to embed languages such as the specification language Z and functional logic programming languages in a complete and natural way. Syntax, semantics and equational theory of micro-Z are defined. Several computation models are developed. The reference computation model, which is based on natural semantics, combines functional reduction and constraint resolution, and leads to an implementation by an abstract machine, which is based on concurrent resolution threads. The results are embedded in the context of the BMBF research project ESPRESS, and have been e.g. applied to the automatization of software tests. All formal material of the thesis is given in type-checked Z, which makes this work also a case study on the usage of Z for problems of meta modeling.