[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


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)}

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 mailing list