Projektstart: 01.01.1997

Projektträger: Universität Augsburg

Projektverantwortung vor Ort: Prof. Dr. Bernhard Möller

Beteiligte WissenschaftlerInnen der Universität Augsburg: Kim Solin

Beteiligte WissenschaftlerInnen / Kooperationen: Prof. Dr. Jules Desharnais (Université Laval) und andere

Zusammenfassung

Die dämonische Refinement-Algebra ist eine Variation der Kleene-Algebra mit Tests. Sie wird verwendet um Aussagen über totale Korrektheit zu beweisen. Prominentestes Beispiel für Refinement-Algebren ist die Algebra der Prädikat-Transformatoren. Solche Transformatoren beschreiben abstrakt Vor- und Nachbedingungen eines Programms und sind deshalb sehr eng mit dem wp/wlp-Kalkül von Dijkstra verwandt.