--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2009 ---
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