--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on January 2009 ---
Regarding my problems with proving the algorithm: false alarm, I forgot to remove the incrementation of the return value, The algorithm is proven so far. But I have an other question regarding the position if incrementation in a loop. The original algorithm of unique_copy reads: int value = a[i_a]; dest[i_dest] = value; while (++i_a != length) { if (!(value == a[i_a])) { value = a[i_a]; dest[++i_dest] = value; } } return ++i_dest; } I moved the first incrementation before the loop, to avoid problems with the loop invariant. I would like to know, if there are consequences for the loop invariants if I increment the index like this. I hope you see my point, Cheers Christoph