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 09:48:44 +0100
  • In-reply-to: <20090119180605.24762f1e@is005115>
  • References: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE> <20090119180605.24762f1e@is005115>
Hello Virgile, and thank you very much for your help.

>
>> The Function:
>>
>> /*@ axiomatic Function_unique_copy {
>>
>>         logic integer function_unique_copy{La,Lb}(int* a, int* b, integer 
>> i_a, integer i_b);
>>
>>         axiom function_unique_copy_empty{La,Lb}:
>>          \forall int* a, int* b, integer i_a, i_b;
>>          0 > i_a && 0 > i_b ==> function_unique_copy{La,Lb}(a, b, i_a, 
>> i_b) == 0;
>
> here, you are saying that function_unique_copy is 0 when both i_a and
> i_b are strictly negative. I'd say that this is true as soon as one of
> the lengths is strictly negative (so I'd have 0>i_a || 0 > i_b)

That is right, I used the wrong operator, I have to correct the other 
specifications I made as well.

>
>>     /*@
>>      requires 0 <= length;
>>      requires \valid_range(a, 0, length-1);
>>      requires \valid_range(dest, 0, length-1);
>>
>>      ensures 0 <= \result <= length;
>>
>>      ensures \result == function_unique_copy{Old,Here}(a, dest, length-1, 
>> \result-1);
>>     */
>>
>> int unique_copy_array(int* a, int length, int* dest)
>> {
>>
>>     int i_a = 0;
>>     int i_dest = 0;
>>
>>     if (length == 0)
>>         return i_dest;
>>
>>     int value = a[i_a];
>>     dest[i_dest] = value;
>>     i_a++;
>>
>
> Without i_dest++ here, you'll be overwriting the first element of dest
> with the first a[i_a] distinct from a[0]. This is consistent with your
> axiomatisation, as function_unique_copy(i_a,i_b,0,0) returns 1
> regardless of the values of i_a[0] and i_b[0], but I'm unsure that this
> is the intended behavior.

That is correct, I made a mistake.
In the if -clause in the loop, i_dest must be iterated before the 
assignment.


>
>>     /*@
>>      loop invariant 0 < i_a <= length;
>>      loop invariant i_dest < i_a;
>>      loop invariant 0 <= i_dest < length;
>>
>>      loop invariant i_dest == function_unique_copy{Pre,Here}(a, dest, 
>> i_a-1, i_dest-1);
>>      */
>
> in the invariant, you do not specify anything about the variable value,
> so that the verification condition generator can't do much with it.
> Possible invariants are:
>
>     loop invariant a[i_a-1] == value;
>     loop invariant i_dest !=0 ==> dest[i_dest-1] == value ;
>
> Note that the guard i_dest !=0 is here because of the special role of
> the dest[0] cell, which will hold successively a[0] and a[i_a] where
> i_a is the smallest index such that a[0] != a[i_a]
>
>>     while (i_a != length)
>>     {
>>         if (!(value == a[i_a]))
>>         {
>>             value = a[i_a];
>>             dest[i_dest] = value;
>
> Apparently Z3 is smart enough to use only the original assertion, but
> alt-ergo and Simplify need some help here (again, the case where i_dest
> is 0 is a bit special)
>
> /*@ assert i_dest ==
> function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1); */
> /*@ assert
> a[i_a] != a[i_a-1] && i_dest!=0 ==> dest[i_dest]!=dest[i_dest-1]; */
>
>>             /*@assert
>>        i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest);
>>       */
>>       ++i_dest;
>>         }
>>
>>
>>         i_a++;
>>     }
>
> I'm unsure of this ++i_dest. In fact i_dest itself meets the
> post-condition, not its successor. Could it be related to the fact that
> i_dest is not incremented before entering the loop?

As mentioned before, I made a mistake adapting the algorithm from the C++ 
STL notaion:

originally the assignments were:

            value = *first;
            *++result = value;

which I translated into:

        value = a[i_a];
        dest[++i_dest] = value;


====

I realized the recommendations you made, ignoring the incorrect 
incrementation of i_dest:
my annotated algorithm reads:

int unique_copy_array(int* a, int length, int* dest)
{
    int i_a = 0;
    int i_dest = 0;

    if (length == 0)
        return i_dest;

    int value = a[i_a];
    dest[i_dest] = value;
    i_a++;

    /*@
     loop invariant 0 < i_a <= length;
     loop invariant i_dest < i_a;
     loop invariant 0 <= i_dest < length;

     loop invariant a[i_a-1] == value;
     loop invariant i_dest !=0 ==> dest[i_dest-1] == value ;

     loop invariant i_dest == function_unique_copy{Pre,Here}(a, dest, i_a-1, 
i_dest-1);
     */
    while (i_a != length)
    {
        if (!(value == a[i_a]))
        {
            value = a[i_a];

            dest[i_dest] = value;

      /*@ assert i_dest ==
        function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1);
      */
      /*@ assert
        a[i_a] != a[i_a-1] && i_dest!=0 ==> dest[i_dest]!=dest[i_dest-1];
      */
     /*@ assert
        i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest);
      */

           ++i_dest;
        }
        i_a++;
    }
    return ++i_dest;
}


But unfortunatly Z3 fails to prove the last post condition.

Could you please show me, what I missed?
___

Now I have corrected the algorithm in a way, that i_dest is incremented 
before the loop.
I have modified the assertions and loop invariants to the new requirements 
of the higher index but Z3 fails to prove the postcondition.
I would like you to have a look on this code and tell me what I missed.

int unique_copy_array(int* a, int length, int* dest)
{
    int i_a = 0;
    int i_dest = 0;

    if (length == 0)
        return i_dest;

    int value = a[i_a];
    dest[i_dest] = value;
    i_a++;
    i_dest++;
    /*@
     loop invariant 0 < i_a <= length;
     loop invariant i_dest <= i_a;
     loop invariant 0 <= i_dest <= length;

     loop invariant a[i_a-1] == value;
     loop invariant dest[i_dest-1] == value ;

     loop invariant i_dest == function_unique_copy{Pre,Here}(a, dest, i_a-1, 
i_dest-1);
     */
    while (i_a != length)
    {
        if (!(value == a[i_a]))
        {
            value = a[i_a];

            dest[i_dest] = value;
      /*@ assert i_dest ==
            function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1);
      */
      /*@ assert
            a[i_a] != a[i_a-1] ==> dest[i_dest] != dest[i_dest-1];
      */
       /*@ assert
            i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest);
      */
           ++i_dest;
        }
        i_a++;
    }
    return ++i_dest;
}

Thanks again for your help,

Cheers
Christoph