--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on January 2009 ---
Hello, I have an algorithm, that copys elements from one array to another, ignoring elements equal to a specific value: To prove the correctness, I have defined a predicate, which is inspired by the nb_occ() predicate given in the acsl implementation document. Unfortunatly, the proof fails in one instance, I would appreciat any help. I also wonder whether numerous indices in axiomatic definitions may lead to difficultys. The algorithm: /*@ axiomatic Predicate_remove_copy { logic integer predicate_remove_copy{La,Lb}(int* a, int* b, integer i_a, integer i_b, int value); axiom predicate_remove_copy_empty{La,Lb}: \forall int* a, int* b, value, integer i_a, i_b; 0 > i_a && 0 > i_b ==> predicate_remove_copy{La,Lb}(a, b, i_a, i_b, value) == 0; axiom predicate_remove_copy_equal_value{La,Lb}: \forall int* a, int* b, value, integer i_a, i_b; 0 <= i_a && \at(a[i_a],La) == value ==> predicate_remove_copy{La,Lb}(a, b, i_a, i_b, value) == predicate_remove_copy{La,Lb}(a, b, i_a-1, i_b, value); axiom predicate_remove_copy_not_equal_value{La,Lb}: \forall int* a, int* b, value, integer i_a, i_b; 0 <= i_a && 0 <= i_b && (\at(a[i_a],La) != value <==> \at(a[i_a],La) == \at(b[i_b],Lb)) ==> predicate_remove_copy{La,Lb}(a, b, i_a, i_b, value) == predicate_remove_copy{La,Lb}(a, b, i_a-1, i_b-1, value)+1; } */ /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (dest, 0, length-1); ensures 0 <= \result <= length; ensures \forall integer k; 0 <= k < \result ==> dest[k] != value; ensures \result == predicate_remove_copy{Old,Here}(a, dest, length-1, \result-1, value); */ int remove_copy_array (int* a, int length, int* dest, int value ) { int i_a = 0; int i_dest = 0; /*@ loop invariant 0 <= i_a <= length; loop invariant i_dest <= i_a; loop invariant 0 <= i_dest <= length; loop invariant \forall integer k; 0 <= k < i_dest ==> dest[k] != value; loop invariant i_dest == predicate_remove_copy{Pre,Here}(a, dest, i_a-1, i_dest-1, value); */ for ( ; i_a != length; ++i_a) if (a[i_a] != value) { dest[i_dest] = a[i_a]; ++i_dest; } return i_dest; } Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090108/05e20a4c/attachment.htm