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

[Frama-c-discuss] WG: Label to refer to a state of the prior iteration



the "state in the previous iteration" for a loop invariant is not 
completely defined: it is meaningless at the first iteration.

However, you might want to specifying properties where the 
initialization is unimportant.
In such a case, you might succeeds by using ghost variables, e.g


int i;
//@ ghost int old_i;

i = 0;


/*@ loop invariant i > 0 ==> old_i == i -1;
    @*/
while (i < 10) {
    ...
    //@ ghost old_i = i;
    i++;
}

Hope this helps,

- Claude


Kerstin Hartig wrote:
> On Christoph Weber's request I forward the following mail:
> ------
>
> Hello,
>
> I am experimenting to prove an algorithm similar to binary_search (lower_bound).
> Currently I would like to "compare" a Variable to itself in the state of the previous iteration.
>
> I would like to know, if such a Label would be of any interest to be implemented or if the concept of adressing the variable in the previous iteration is flawed and should not longer be regarded.
>
> I hope I made my question clear.
>
> Sincerely
>
> Christoph Weber
>
>
> _______________________________________________
> 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                    |