[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