Wp-Kalkül
aus Wikipedia, der freien Enzyklopädie
 |
Der korrekte Titel dieses Artikels lautet „wp-Kalkül“. Diese Schreibweise ist aufgrund technischer Einschränkungen derzeit nicht möglich. |
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] Siehe auch
[Bearbeiten] Literatur
- Edsger W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.
- David Gries, The Science of Programming, Springer, 1981.
