--- layout: fc_discuss_archives title: Message 27 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 Christoph,

[disclaimer: I'm not sure I've understood the axiomatisation of
function_unique_copy. If there's some misinterpretation on my side,
please tell me so]

Le lun 19 jan 2009 08:49:54 CET,
"Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :

> 
> I would like to know if something needs to be added to get the proof or if the axiomatization I chose is inconsistent.
> 

> 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)

>     /*@
>      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.

>     /*@
>      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?

>     return ++i_dest;
> } 
> 

-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83