Axiom: Zuweisung

{ N [x := A] } x = A { N }

Beispiel: zeige {x < 0 und y > 0} x = y - x; {x > 0}

N = (x > 0), A = (y - x)

N [x := A ] = (x > 0) [x := (y-x) ]
            = (y-x) > 0 = (y > x)

{ y > x } x = y - x { x > 0 }

{x < 0 und y > 0} ist eine Verschärfung der Vorbedingung {y > x}



Johannes Waldmann 2004-06-30