Content deleted Content added
m corrected formatting, made explanation of example more thorough |
No edit summary |
||
Line 3:
The canonical ''predicate transformer'' of sequential imperative programming is the so-called "weakest pre-condition" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "post-condition". 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 asignment statment:
:<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''.
| |||