Content deleted Content added
m correction to reference |
m Made example calculation more explicit and added explanation of example. |
||
Line 9:
An example of a valid calculation of ''wp'' for assignments with integer valued variables ''x'' and ''y'' is:
:<math>wp(x := y - 5, x > 10) = (y - 5 > 10) = (y > 15) </math>
This means that in order for the ''post-condition x > 10'' to be true after the assignment, the ''pre-condition y > 15'' must be true before the assignment.
Dijkstra also defined alternative ('''if''') and repetitive ('''do''') constructs as well as a composition operator (''';''') using ''wp''. The alternative and repetitive constructs used ''guarded commands'' to influence execution. Because of the rules he imposed on the definition of ''wp'', both constructs allow for non-deterministic execution if the ''guards'' in the commands are non disjoint.
| |||