Algebraic foundations of the unifying theories of programming [Elektronische Ressource] / Walter Guttmann

Algebraic Foundations of theUnifying Theories of ProgrammingDissertationzur Erlangung des Doktorgrades Dr. rer. nat.der Fakultat fur Ingenieurwissenschaften und Informatikder Universitat UlmWalter Guttmannaus Gro wardeinUniversitat UlmFakultat fur Ingenieurwissenschaften und InformatikInstitut fur Programmiermethodik und CompilerbauDirektor: Prof. Dr. Helmuth A. Partsch2007Amtierender Dekan: Prof. Dr. Helmuth A. PartschErster Gutachter: Prof. Dr. Helmuth A. PartschZweiter Gutachter: Prof. Dr. Friedrich W. von HenkeDritter Gutachter: Prof. Dr. Bernhard MollerTag der Promotion: 5. Dezember 2007AbstractHoare and He’s Unifying Theories of Programming take a relational view on semantics. Themeaning of a non-deterministic, imperative program is described by ‘designs’ composed oftwo relations. They represent terminating states and relate the initial and nal values ofthe observable variables, respectively. Several ‘healthiness conditions’ are imposed by thetheory to obtain properties found in practice.This work determines the structure of designs and modi es the theory to support non-strict computations. It achieves these goals by identifying healthiness conditions and relatedaxioms that involve unnecessary restrictions and subsequently removing them. The outcomeprovides a clear account of the algebraic foundations of the Unifying Theories of Program-ming.