[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.)

Alan



More information about the Why3-club mailing list