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

Nuno Gaspar nmpgaspar at gmail.com
Wed Mar 26 15:43:04 CET 2014


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>:

> 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
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140326/d99bd3cf/attachment.html>


More information about the Why3-club mailing list