--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on December 2008 ---
Hallo Christoph, Le mer 10 d?c 2008 13:58:59 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > 1. while exploring axiomatic definitions I discovered, defining a variable "null" causes Problems, obviously it interferes with the "\null" but I would like to be able to use "null" nevertheless. > That's not normal. Can you be more specific about the troubles you have with using a variable called null (and which frama-c version you're using)? The current development version seems to be fine with this respect. > /*@ > loop invariant 0 <= index_a <= length_a; > loop invariant 0 <= index_b <= length_b; > loop invariant \forall integer k2; \exists integer k1; > > 0 <= k2 < index_b && 0 <= k1 < index_a ==> > nb_occ(b, 0, index_b, b[k2]) == nb_occ(a, 0, index_a, a[k1]); > */ > while (index_a != length_a) > { > if (b[index_b] < a[index_a]) > break; > else if (a[index_a] < b[index_b]) > ++index_a; > else > { > ++index_a; > ++index_b; > } > if (index_b == length_b) return 1; > } > return 0; > } > > I understand that nb_occ might cause the solver the same problems, it caused in the remove_copy algorithm. > > But I don't understand, why > loop invariant 0 <= index_a <= length_a; > loop invariant 0 <= index_b <= length_b; > wont get proven. I guess the problem lies in the invariant for index_b, which is too weak. Namely, if you start a loop step with index_b == length_b (which is fine as far as the invariant is concerned), you might increment index_b, and thus, since you return only in the case where index_b and length_b are equal, you end up with index_b > length_b at the next step, so that the invariant is broken. It is thus a good point for jessie that you can not prove it. Note that there is no issue with index_a since the equality test with length_a occurs before the incrementation. A loop invariant 0 <= index_b < length_b would be better, but for that you need to require that length_b > 0 (otherwise the invariant might not hold at the beginning of the loop). > 3. An other algorithm I defined uses two for-loops: > I would like to know, what can be done to help the proover to master the difficult quantified expressions. I have to admit that I haven't looked to closely at your specification, but it usually helps to provide some assertions inside the loop. -- E tutto per oggi, a la prossima volta. Virgile