--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2008 ---
Hello again, I would like to report some other things I came across and ask some questions as well: 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. 2. I have an includes algorithm: It returns a "true" if all the elements of range "b" are present in range "a" with exactly the same quantity. /*@ predicate ascending_array{Here}(int* a, integer length) = \forall integer k1, k2; 0 <= k1 <= k2 < length ==> a[k1] <= a[k2]; */ /*@ requires 0 <= length_a; requires 0 <= length_b; requires \valid_range (a, 0, length_a); requires \valid_range (b, 0, length_b); requires ascending_array(a, length_a); requires ascending_array(b, length_b); ensures \forall integer k2; \exists integer k1; 0 <= k2 < length_b && 0 <= k1 < length_a ==> nb_occ(b, 0, length_b, b[k2]) == nb_occ(a, 0, length_a, a[k1]); */ int includes_array(int* a , int length_a , int* b, int length_b ) { int index_a = 0; int index_b = 0; /*@ 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. 3. An other algorithm I defined uses two for-loops: find_first_of_array returns an index to the first element in the range "a", that is equal to some element in range "b": /*@ requires 0 <= length_a; requires 0 <= length_b; requires \valid_range (a, 0, length_a); requires \valid_range (b, 0, length_b); ensures 0 <= \result <= length_a; ensures \exists integer k2; \forall integer k1; 0 <= k1 < \result && 0 <= k2 < length_b ==> a[k1] != a[k2]; behavior found: ensures \exists integer k1, k2; 0 <= k1 < length_a && 0 <= k2 < length_b ==> a[\result] == a[k1] == b[k2]; */ int find_first_of_array (int* a, int length_a, int* b, int length_b) { int index_a = 0; int index_b = 0; /*@ loop invariant 0 <= index_a <= length_a; loop invariant 0 <= index_b <= length_b; loop invariant \forall integer k1; \exists integer k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != a[k2]; for found: loop invariant \forall integer k1, k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != b[k2]; */ for ( ; index_a != length_a; ++index_a ) { index_b = 0; /*@ loop invariant 0 <= index_a <= length_a; loop invariant 0 <= index_b <= length_b; loop invariant \exists integer k2; \forall integer k1; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != a[k2]; for found: loop invariant \forall integer k1, k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != b[k2]; */ for (; index_b != length_b; ++index_b) if (b[index_b] == a[index_a]) return index_a; } return length_a; } I would like to know, what can be done to help the proover to master the difficult quantified expressions. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081210/06f9a92c/attachment.htm