[Why3-club] Specifying the order in which loop invariant may be proven
Alan Schmitt
alan.schmitt at polytechnique.org
Wed Mar 26 15:31:09 CET 2014
Hello,
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:
#+begin_src why3
for i = 0 to n do
invariant {I(i)}
invariant {J(i)}
...
done
#+end_src
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)?
Thanks,
Alan
More information about the Why3-club
mailing list