--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2009 ---
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 |