Diese Seite auf deutsch
SearchRefinement Algebra
| Start date: | 01.01.1997 |
| Funded by: | Universität Augsburg |
| Local project leader: | Prof. Dr. Bernhard Möller |
| Local scientists: |
Kim Solin |
| External scientists / cooperations: |
Prof. Dr. Jules Desharnais (Université Laval) and others |
| Publications: | Publication list |
Abstract
The demonic refinement algebra is a variant of Kleene algebra with tests.
It is used to verify properties for total correctness.
One of the most famous models are predicate transformers.
They describe pre- and postconditions of a given program in an abstract manner and are closely related to the wp/wlp-calculus of Dijkstra.