--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on January 2009 ---
Hello Christoph, [disclaimer: I'm not sure I've understood the axiomatisation of function_unique_copy. If there's some misinterpretation on my side, please tell me so] Le lun 19 jan 2009 08:49:54 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > > 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; 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) > /*@ > 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. > /*@ > 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? > return ++i_dest; > } > -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 71 83