Content deleted Content added
m Minor tidying |
m Minor format tidying |
||
Line 3:
The canonical ''predicate transformer'' of sequential imperative programming is the so-called "[[weakest precondition]]" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "[[postcondition]]". The result of applying this function gives the "weakest pre-condition" for ''S'' terminating with ''R'' true. An example is the following definition of the assignment statement:
:<math> wp(x := E, R)\ =\ R_E^x </math>
This gives a predicate that is a copy of ''R'' with the value of ''x'' replaced by ''E''.
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. This is also the "weakest pre-condition", in that it is the "weakest" restriction on the value of ''y'' which makes ''x > 10'' true after the assignment.
| |||