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.
