Content deleted Content added
Line 50:
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 ==
| |||