Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-102
Main Title: A set-based calculus and its implementation
Translated Title: Ein mengenbasierter Kalkül und seine Implementierung
Author(s): Grieskamp, Wolfgang
Advisor(s): Pepper, Peter
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: 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.
URI: urn:nbn:de:kobv:83-opus-77
http://depositonce.tu-berlin.de/handle/11303/399
http://dx.doi.org/10.14279/depositonce-102
Exam Date: 26-Nov-1999
Issue Date: 28-Jul-2000
Date Available: 28-Jul-2000
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Ausführbare Spezifikationen
Berechnung
Mengenbasierte Sprachen
Nebenläufige Resolution
Z Notation
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_9.pdf2.82 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.