Nächste Seite: Axiom für Schleifen Aufwärts: Semantik von Programmiersprachen Vorherige Seite: Eiffel
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 }