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

Alan Schmitt alan.schmitt at polytechnique.org
Wed Mar 26 16:13:31 CET 2014


Nuno Gaspar <nmpgaspar at gmail.com> writes:

> not exactly what you want, but
>
> invariant {I(i+1) -> J(i)}
>
> wouldn't do?

I'm afraid that "I(i) -> J(i)" would not work as I still would not have
"I(i+1)" as hypothesis to prove "J(i+1)".

Thanks,

Alan



More information about the Why3-club mailing list