Predicate transformer semantics: Difference between revisions

Content deleted Content added
Line 170:
= { repetition rule }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ]
= { assignment rule, found wpL = Z(x ← x-1) }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post]
= { substitution }
the strongest solution of
Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ]
= { solve the equation by approximation }
post(x ← 0)