{ 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}