Das Kefk Network Wiki befindet sich im Testbetrieb.
Wp-Kalkül
Aus Kefk.
| Bild:Icon falscher Titel.svg | Der korrekte Titel dieses Artikels lautet „wp-Kalkül“. Diese Schreibweise ist aufgrund technischer Einschränkungen 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.
Siehe auch
Literatur
- Edsger W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.
- David Gries, The Science of Programming, Springer, 1981.
 | Dieses Dokument entstammt in seiner ersten oder einer späteren Version der deutschsprachigen Wikipedia. Es ist dort zu finden unter dem Stichwort Wp-Kalk%C3%BCl, die Liste der bisherigen Autoren befindet sich in der Versionsliste; die Originalfassung kann dort auch bearbeitet werden. Alle Texte der Wikipedia und ihre Derivate stehen unter der GNU-Lizenz für freie Dokumentation. |
