--- layout: fc_discuss_archives title: Message 28 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"



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