Axiomatische Semantik

Notation für Aussagen über Programmzustände:

{ V } A { N }

• für jeden Zustand s, in dem Vorbedingung V gilt:
• wenn Anweisung A ausgeführt wird,
• und Zustand t erreicht wird, dann gilt dort Nachbedingung N

Beispiel:

{ x >= 5 } y := x + 3 { y >= 7 }

Gültigkeit solcher Aussagen kann man

• beweisen (mit Hoare-Kalkül)
• prüfen (testen)