--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on January 2009 ---
Hello, some days ago, I committed an algorithm "unique_copy". After some corrections, the algorithm was proven. But to position of the incrementation was modified. I restored the original algorithm and adapted the loop invariants: My problem is now, that a VC fails to proof and I have no Idea why. I would like you to have a look and tell me, what needs to be corrected. ===================== /*@ axiomatic Specification_unique_copy { logic integer spec_unique_copy{La,Lb}(int* a, integer i, int* b, integer j); axiom unique_copy_empty{La,Lb}: \forall int* a, int* b, integer i, j; 0 > i || 0 > j ==> spec_unique_copy{La,Lb}(a, i, b, j) == 0; axiom unique_copy_first_element{La,Lb}: \forall int* a, int* b, integer i, j; 0 == i ==> spec_unique_copy{La,Lb}(a, i, b, j) == spec_unique_copy{La,Lb}(a, i-1, b, j-1) + 1; axiom unique_copy_equal{La,Lb}: \forall int* a, int* b, integer i, j; 0 < i && \at(a[i],La) == \at(a[i-1],La) ==> spec_unique_copy{La,Lb}(a, i, b, j) == spec_unique_copy{La,Lb}(a, i-1, b, j); axiom unique_copy_not_equal{La,Lb}: \forall int* a, int* b, integer i, j; 0 < i && 0 <= j && (\at(a[i],La) != \at(a[i-1],La) <==> \at(a[i],La) == \at(b[j],Lb)) ==> spec_unique_copy{La,Lb}(a, i, b, j) == spec_unique_copy{La,Lb}(a, i-1, b, j-1) + 1; axiom unique_copy_not_equal_label{La,Lb1,Lb2}: \forall int* a, int* b, integer i, j; (\forall integer i; 0<= i <= j ==> \at(b[i],Lb1) == \at(b[i],Lb2)) ==> spec_unique_copy{La,Lb1}(a, i, b, j) == spec_unique_copy{La,Lb2}(a, i, b, j); } */ /*@ predicate disjoint_arrays(int* a, int* b, integer n) = \forall integer i, k; 0 <= i < n && 0 <= k < n ==> a + i != b + k; */ /*@ requires 0 <= length; requires \valid_range(a, 0, length-1); requires \valid_range(b, 0, length-1); requires disjoint_arrays(a,b,length); ensures 0 <= \result <= length; ensures \result == spec_unique_copy{Old,Here}(a, length-1, b, \result-1); */ int unique_copy_array(int* a, int length, int* b) { int i = 0; int j = 0; if (length == 0) return j; int value = a[i]; b[j] = value; /*@ loop invariant 0 <= i < length; loop invariant j <= i; loop invariant 0 <= j < length; loop invariant a[i] == value; loop invariant b[j] == value ; loop invariant j == spec_unique_copy{Pre,Here}(a, i-1, b, j-1); */ while (++i != length) { if (!(value == a[i])) { value = a[i]; b[++j] = value; /*@ assert a[i] != a[i-1] ==> b[j] != b[j-1]; */ /*@ assert j+1 == spec_unique_copy{Pre,Here}(a, i, b, j); */ } } return ++j; } ========== I would also like to know, why adding following requirement will cause loop invariants to fail: requires disjoint_arrays(a, b, length); Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/cc293c17/attachment.htm