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: Mon, 19 Jan 2009 08:49:54 +0100
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