Content deleted Content added
Line 166:
= { 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
| |||
Line 166:
= { 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
| |||