Nächste Seite: Axiom für Schleifen Aufwärts: Semantik von Programmiersprachen Vorherige Seite: Bsp: Operationale 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
{ N[x/E] } x := E { N }
{ V und B } C { N }
und { V und not B } D { N }
=> { V } if (B) then C else D { N }