[Why3-club] Specifying the order in which loop invariant may be proven
alan.schmitt at polytechnique.org
Wed Mar 26 15:31:09 CET 2014
It seems to me that when several invariants are given for a loop, each
one is proven separately assuming every invariant at the previous step.
For instance, in the following:
for i = 0 to n do
one has to prove I(i+1) assuming I(i) and J(i), and the same for J(i+1).
Is it possible to rely on the order in which the invariants are given,
such that I(i+1) is proven I(i) and J(i), as before, but J(i+1) is
proven using I(i+1) and J(i)?
More information about the Why3-club