Notation für Aussagen über Programmzustände:
{ V } A { N }
- für jeden Zustand s
mathend000#,
in dem Vorbedingung V
mathend000# gilt:
- wenn Anweisung A ausgeführt wird,
- und Zustand t
mathend000# erreicht wird,
dann gilt dort Nachbedingung N
mathend000#
Beispiel:
{ x >= 5 } y := x + 3 { y >= 7 }
Gültigkeit solcher Aussagen kann man
- beweisen (mit Hoare-Kalkül)
- prüfen (testen)
Johannes Waldmann
2014-03-31