3
$\begingroup$

I am interested in computing weakest preconditions (WP) of loops.

If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I is (as discussed here):

WP(while E do S done, R) = 
    (1) I
AND (2) for all y, ((E /\ I) => WP(S,I /\ x<y))[y/x]
AND (3) for all y, ((not E /\ I) => R)[y/x]

I understand that it is not easy to get automatically the WP without annotating with an invariant, but how do we know that it is the weakest possible precondition ? Also, is it really impossible, by using different invariants, to get different preconditions with this definition?

In another textbook, I have the following definition:

WP(while E do S done, R) = I
if we can prove separately:
(1) (E /\ I /\ V=n) => WP(S, I /\ V<n)
(2) I => V>=0
(3) (not E /\ I) => R

Are these definitions equivalent? In this definition, and if we prove the conditions 1-3 separately, is I really the weakest precondition, or a stronger approximate of the true WP? It looks at first sight that this rule is easier to understand because there is no 1st order in the precondition, but how is it different?

I guess the question behind all this would be : given a simple example of code with a loop, what would be the easiest way to compute the weakest precondition?

Improve this question
$\endgroup$
1
  • $\begingroup$ Yes sure, sorry for that I edited the post. $\endgroup$
    – Zooky
    Dec 3, 2017 at 8:51

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.