Predicate transformer semantics: Difference between revisions

Revision as of 11:03, 29 November 2022

Revision as of 11:05, 29 November 2022

Line 167:

wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥ 0 ∧ post)

= { sequential composition, goto, assignment rules }

wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post)

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