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

Alan Schmitt alan.schmitt at polytechnique.org
Wed Mar 26 16:12:36 CET 2014

Claude Marche <Claude.Marche at inria.fr> writes:

> Hi,
> I think
>    invariant { I(i) && J(i) }
> is what you look for.

That works, thanks a lot! (And I tried "/\" and it did not ... this is
quite a big difference between the two.)


More information about the Why3-club mailing list