Wand's Beispiel

{ R(x) }

while not(Z0(x) or Z1(x))

do { I(x) }

x := f(x)

{ Z0(x) }

Invariante

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen