# [Why3-club] Specifying the order in which loop invariant may be proven

Claude Marche Claude.Marche at inria.fr
Wed Mar 26 15:52:06 CET 2014

```
Hi,

I think

invariant { I(i) && J(i) }

is what you look for.

- Claude

On 03/26/2014 03:43 PM, Nuno Gaspar wrote:
> not exactly what you want, but
>
> invariant {I(i+1) -> J(i)}
>
> wouldn't do?
>
>
>
>
>
>
>
> 2014-03-26 15:31 GMT+01:00 Alan Schmitt <alan.schmitt at polytechnique.org
> <mailto:alan.schmitt at polytechnique.org>>:
>
>     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
>
>     _______________________________________________
>     Why3-club mailing list
>     Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr>
>     http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
>
>
>
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made \$600
> dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible
> life choice.
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>

```