--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on January 2009 ---
Hello Virgile, and thank you very much for your help. > >> 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; > > here, you are saying that function_unique_copy is 0 when both i_a and > i_b are strictly negative. I'd say that this is true as soon as one of > the lengths is strictly negative (so I'd have 0>i_a || 0 > i_b) That is right, I used the wrong operator, I have to correct the other specifications I made as well. > >> /*@ >> 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++; >> > > Without i_dest++ here, you'll be overwriting the first element of dest > with the first a[i_a] distinct from a[0]. This is consistent with your > axiomatisation, as function_unique_copy(i_a,i_b,0,0) returns 1 > regardless of the values of i_a[0] and i_b[0], but I'm unsure that this > is the intended behavior. That is correct, I made a mistake. In the if -clause in the loop, i_dest must be iterated before the assignment. > >> /*@ >> 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); >> */ > > in the invariant, you do not specify anything about the variable value, > so that the verification condition generator can't do much with it. > Possible invariants are: > > loop invariant a[i_a-1] == value; > loop invariant i_dest !=0 ==> dest[i_dest-1] == value ; > > Note that the guard i_dest !=0 is here because of the special role of > the dest[0] cell, which will hold successively a[0] and a[i_a] where > i_a is the smallest index such that a[0] != a[i_a] > >> while (i_a != length) >> { >> if (!(value == a[i_a])) >> { >> value = a[i_a]; >> dest[i_dest] = value; > > Apparently Z3 is smart enough to use only the original assertion, but > alt-ergo and Simplify need some help here (again, the case where i_dest > is 0 is a bit special) > > /*@ assert i_dest == > function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1); */ > /*@ assert > a[i_a] != a[i_a-1] && i_dest!=0 ==> dest[i_dest]!=dest[i_dest-1]; */ > >> /*@assert >> i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest); >> */ >> ++i_dest; >> } >> >> >> i_a++; >> } > > I'm unsure of this ++i_dest. In fact i_dest itself meets the > post-condition, not its successor. Could it be related to the fact that > i_dest is not incremented before entering the loop? As mentioned before, I made a mistake adapting the algorithm from the C++ STL notaion: originally the assignments were: value = *first; *++result = value; which I translated into: value = a[i_a]; dest[++i_dest] = value; ==== I realized the recommendations you made, ignoring the incorrect incrementation of i_dest: my annotated algorithm reads: 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 a[i_a-1] == value; loop invariant i_dest !=0 ==> dest[i_dest-1] == value ; 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 == function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1); */ /*@ assert a[i_a] != a[i_a-1] && i_dest!=0 ==> dest[i_dest]!=dest[i_dest-1]; */ /*@ assert i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest); */ ++i_dest; } i_a++; } return ++i_dest; } But unfortunatly Z3 fails to prove the last post condition. Could you please show me, what I missed? ___ Now I have corrected the algorithm in a way, that i_dest is incremented before the loop. I have modified the assertions and loop invariants to the new requirements of the higher index but Z3 fails to prove the postcondition. I would like you to have a look on this code and tell me what I missed. 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++; i_dest++; /*@ loop invariant 0 < i_a <= length; loop invariant i_dest <= i_a; loop invariant 0 <= i_dest <= length; loop invariant a[i_a-1] == value; loop invariant dest[i_dest-1] == value ; 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 == function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1); */ /*@ assert a[i_a] != a[i_a-1] ==> dest[i_dest] != dest[i_dest-1]; */ /*@ assert i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest); */ ++i_dest; } i_a++; } return ++i_dest; } Thanks again for your help, Cheers Christoph