--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Loop invariants





Hollas Boris (CR/AEY1) wrote:
> Hello,
> 
> consider the following while loop:
> 
> 
> // loop invariant i <= n;
> while(some condition) {
>   P
>   i++;
> }
> 
> 
> Assume that
> - the loop invariant holds and
> - P is a block of code that does not modify i.
> Hence, i < n holds in P. 
 >
 >Does Jessie know that when analysing this kind of loop? Ie, is Jessie 
able to conclude  i <= n \land (some condition) ==> i < n ?

Sure if condition is (i < n) or anything that implies (i < n), but 
otherwise no. But if you are able to prove that the invariant holds, 
then certainly you should be able to prove //@ assert i<n; either before 
or after P, no ?

What is your condition exactly ?

> - Boris
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |