Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] new axiomatic "function"
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Tue, 20 Jan 2009 10:02:40 +0100
  • In-reply-to: <F16093DB046C44AD9FEFA9A4316A1805@AHARDPLACE>
  • References: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE><20090119180605.24762f1e@is005115> <F16093DB046C44AD9FEFA9A4316A1805@AHARDPLACE>
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