Predicate transformer semantics: Difference between revisions

Revision as of 10:42, 29 November 2022

Revision as of 10:46, 29 November 2022

Line 167:

= { sequential composition and alternation rules }

''<math>wp(do x > 0 \rightarrow L: x := x-1 od, (x<0 \wedge wp(x := -x; goto L, post)) \vee

(x >= 0 \wedge post)</math>''

= { sequential composition, goto, assignment rules }