--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on December 2008 ---
Hello again, and thank you for the continuing help. Regardless of the code, I want to proof a postcondition for a remove_copy algorithm: int remove_copy_array (int* a, int length, int* dest, int value ) { int index_a = 0; int index_dest = 0; for ( ; index_a != length; ++index_a) if (a[index_a] != value) { dest[index_dest] = a[index_a]; ++index_dest; } return index_dest; } This algorithm copies every element from range a to range dest. So far i can proof that value does not appear in dest: ensures \forall integer k; 0 <= k < \result ==> dest[k] != value; And that \result (==length of the dest-range) is equal to the length of the range a minus the number of occurrences of value: ensures \result == length - nb_occ{Old}(a, 0, length-1, value); What I want to proof now, is that all the other elements from range a have been copied to range dest. Since multiple occurrences of the same element are allowed, a simple "check" via an \exists-quantifier is not sufficient. I also have to proof, that the number of equal elements in both arrays are equal. I can proof, that at least one occurence has been copied: ensures \forall integer m; 0 <= m < \result ==> ( \exists integer n; 0 <= n < length && dest[m] == a[n] ); But if I try to proof the equivalence of occurences of equal elements, I get problems: ensures \forall integer m; 0 <= m < \result ==> ( \exists integer n; 0 <= n < length && (dest[m] == a[n] ==> nb_occ{Here}(dest, 0, \result-1, dest[m]) == nb_occ{Old}(a, 0, length-1, a[n]))); I believe, that dest[m] and a[n] can differ in each iteration and therefore it is not possible to get a consistent loop invariant. To get something like this to work, I would need to span a tree for every possible element and "count" the depth. I dont't believe that this works. What I would like to know is, if there is a possibility to formulate what i intent. By the way: /*@ axiomatic NbOcc { logic integer nb_occ{L}(int* a, integer _null, integer index, int value); axiom nb_occ_empty{L}: \forall int* a, int value, integer _null, index; _null > index ==> nb_occ(a,_null,index,value) == 0; axiom nb_occ_true{L}: \forall int* a, int value, integer _null, index; _null <= index && a[index] == value ==> nb_occ(a,_null,index,value) == nb_occ(a,_null,index-1,value) + 1; axiom nb_occ_false{L}: \forall int* a, int value, integer _null, index; _null <= index && a[index] != value ==> nb_occ(a,_null,index,value) == nb_occ(a,_null,index-1,value); } */ Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081218/c356b438/attachment-0001.htm