Axiomatische Semantik

Hoare-Kalkül

{ V } A { N }

(Wenn V gilt, dann A ausgeführt wird, gilt danach N.)

Kalkül: für jede Anweisung ein Axiom, das die schwächste Vorbedingung (weakest precondition) beschreibt.

Beispiele

• wp(x : = E, N) = N[x/E]
• wp(if (B) then C else D, N) = B $\wedge$ wp(C, N) $\vee$ ¬B $\wedge$ wp(D, N)
• Schleife ...benötigt Invariante

(siehe Vorlesung Verifikation)