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

[Frama-c-discuss] new axiomatic "function"



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