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

(siehe Vorlesung Verifikation)



Johannes Waldmann 2007-01-23