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?