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: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 19 Jan 2009 18:06:05 +0100
  • In-reply-to: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE>
  • References: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE>
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