wp-Kalkül
aus Wikipedia, der freien Enzyklopädie
Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung.
Die Überprüfung der Korrektheit geschieht durch Rückwärtsanalyse des Programmcodes. Ausgehend von der Nachbedingung wird geprüft, ob diese durch die Vorbedingung und den Programmcode garantiert wird.
Alternativ kann auch der Hoare-Kalkül benutzt werden, bei dem im Gegensatz zum wp-Kalkül eine Vorwärtsanalyse stattfindet.
[Bearbeiten] Literatur
- Edsger W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.
- David Gries, The Science of Programming, Springer, 1981.
