Content deleted Content added
Line 44:
[[User:Houseofwealth|Houseofwealth]] ([[User talk:Houseofwealth|talk]]) 00:56, 5 March 2015 (UTC)
The middle clause of the wlp doesn't guarantee that the whole wlp is still true after the first iteration (when E is true at first), only the invariant, which makes it too weak.
For instance, with the following program and given some valid invariant I (just True?)
while x < 2 do x := x+1 done
The state <code>{x = 0}</code> should satisfy the wlp <math>I \wedge (E \Rightarrow I[x \leftarrow x+1] \wedge \dots)</math>, for any tautology R, so the first and second clauses are true, and the last one is actually true independently of the value of R; so we can replace it with an unsatisfiable postcondition <math>(x = 42)</math>, and our wlp would still hold; even though it should never do, as the loop always terminates. A universal quantification like in the total correctness subsection seems necessary here as well.
== Stongest postconditions are missing a motivation ==
| |||