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



Salut,


some time ago, I posted an annotated function "remove_copy".

To get the proof, an axiom and an assertion had to be added.
Today, I would like to post a modification of this algorithm.
This one is called "unique_copy". It copies elements from a source array to a destination array.
If consecutive elements are equal, only the first one is copied.

I modified the annotation from remove_copy accordingly. This time, each element is compared with its predecessor.

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;

    axiom function_unique_copy_first_element{La,Lb}:
         \forall int* a, int* b, integer i_a, i_b;
         0 == i_a ==>
         function_unique_copy{La,Lb}(a, b, i_a, i_b) ==
         function_unique_copy{La,Lb}(a, b, i_a-1, i_b-1) + 1;
         
        axiom function_unique_copy_equal{La,Lb}:
         \forall int* a, int* b, integer i_a, i_b;
         0 < i_a &&
         \at(a[i_a],La) == \at(a[i_a-1],La) ==>
         function_unique_copy{La,Lb}(a, b, i_a, i_b) ==
         function_unique_copy{La,Lb}(a, b, i_a-1, i_b);

         axiom function_unique_copy_not_equal{La,Lb}:
         \forall int* a, int* b, integer i_a, i_b;
         0 < i_a && 0 <= i_b &&
         (\at(a[i_a],La) != \at(a[i_a-1],La) <==> \at(a[i_a],La) == \at(b[i_b],Lb)) ==>
         function_unique_copy{La,Lb}(a, b, i_a, i_b) ==
         function_unique_copy{La,Lb}(a, b, i_a-1, i_b-1) + 1;
       
    
    axiom function_unique_copy_not_equal_label{La,Lb1,Lb2}:
         \forall int* a, int* b, integer i_a, i_b;
         (\forall integer i; 0<= i <= i_b ==> 
            \at(b[i],Lb1) == \at(b[i],Lb2)) ==>
         function_unique_copy{La,Lb1}(a,b,i_a,i_b) ==
         function_unique_copy{La,Lb2}(a,b,i_a,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++;

    /*@
     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);
     */
    while (i_a != length)
    {
        if (!(value == a[i_a]))
        {
            value = a[i_a];
            dest[i_dest] = value;
            /*@assert
       i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest);
      */
      ++i_dest;
        }
       

        i_a++;
    }
    return ++i_dest;
} 


I appreciate the help


Cheers
Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090119/13e05000/attachment.htm