Predicate transformer semantics: Difference between revisions

Revision as of 11:05, 29 November 2022

Revision as of 11:08, 29 November 2022

Line 172:

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

Therefore, wp(prog2, post ) = post(x← 0) .

== Other predicate transformers ==