Axiomatische Semantik

Notation für Aussagen über Programmzustände:

{ V } A { N }

• für jeden Zustand s, in dem Vorbedingung V gilt:
• wenn A (Anweisung) ausgeführt wird,
• gilt im erreichten Zustand t die Nachbedingung N

Beispiel:

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

Gültigkeit solcher Aussagen kann man

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