• English
    • Deutsch
  • English 
    • English
    • Deutsch
  • Login
View Item 
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Algebraic foundations of the Unifying Theories of Programming

Thumbnail
vts_6099_8221.pdf (862.7Kb)
95 Seiten
Veröffentlichung
2007-12-18
Authors
Guttmann, Walter
Dissertation


Faculties
Fakultät für Ingenieurwissenschaften und Informatik
Abstract
Hoare and He´s Unifying Theories of Programming take a relational view on semantics. The meaning of a non-deterministic, imperative program is described by "designs" composed of two relations. They represent terminating states and relate the initial and final values of the observable variables, respectively. Several "healthiness conditions" are imposed by the theory to obtain properties found in practice. This work determines the structure of designs and modifies the theory to support non-strict computations. It achieves these goals by identifying healthiness conditions and related axioms that involve unnecessary restrictions and subsequently removing them. The outcome provides a clear account of the algebraic foundations of the Unifying Theories of Programming. One of the results is a generalisation of designs by constructing them on semirings with ideals, structures having fewer axioms than relations. This clarifies the essential algebraic structure of designs, allows the reuse of existing mathematical theory and connects to further semantical approaches. The framework is extended by algebraic formulations of finite and infinite iteration, domain, pre-image, determinacy, invariants and convergence. Calculations and reasoning become simpler by the new, more abstract representation as is shown by applying the theory to investigate linear recursions. Another result is an extension of the Unifying Theories of Programming to deal with undefined values irrespective of non-termination. Besides being closer to practice, it forms the basis of a new theory of relations representing non-strict computations. They satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form. Programs can then be executed according to the principle of lazy evaluation, otherwise known from functional programming languages.
Date created
2007
Subject headings
[GND]: Algebraische Struktur | Axiomatische Semantik | Formale Semantik | Funktionale Programmierung | Halbring | Kleene-Algebra | Lineare Rekursion | Nichtdeterminismus | Programmierparadigma | Programmiersprache | Relation <Mathematik> | Relationenalgebra
[LCSH]: Relation algebras
[DDC subject group]: DDC 004 / Data processing & computer science
License
Standard (Fassung vom 03.05.2003)
https://oparu.uni-ulm.de/xmlui/license_v1

Metadata
Show full item record

DOI & citation

Please use this identifier to cite or link to this item: http://dx.doi.org/10.18725/OPARU-895

Guttmann, Walter (2007): Algebraic foundations of the Unifying Theories of Programming. Open Access Repositorium der Universität Ulm und Technischen Hochschule Ulm. Dissertation. http://dx.doi.org/10.18725/OPARU-895
Citation formatter >



Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement
 

 

Advanced Search

Browse

All of OPARUCommunities & CollectionsPersonsInstitutionsPublication typesUlm SerialsDewey Decimal ClassesEU projects UlmDFG projects UlmOther projects Ulm

My Account

LoginRegister

Statistics

View Usage Statistics

Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement