[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
>
More information about the Why3-club
mailing list