--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2010 ---
Hi, here is a specification and implementation of the function adjacent_find that returns the smallest index i of of an array a where a[i] == a[i+1] holds. If no such index exists it returns the length of the array. (It's a simplified version of the C++ standard algorithms http://www.sgi.com/tech/stl/adjacent_find.html) /*@ predicate have_equal_neighbours{Label}(int* a, int n) = \exists int i; 0 <= i < n-1 && a[i] == a[i+1]; */ /*@ requires 0 <= n; requires \valid_range(a, 0, n); assigns \nothing; behavior some: assumes have_equal_neighbours(a, n); ensures 0 <= \result < n-1; ensures a[\result] == a[\result+1]; ensures !have_equal_neighbours(a, \result); behavior none: assumes !have_equal_neighbours(a, n); ensures \result == n; complete behaviors some, none; disjoint behaviors some, none; */ int adjacent_find(int* a, int n) { if (0 == n) return n; /*@ loop invariant 0 <= i < n; loop variant n-i; loop invariant !have_equal_neighbours(a, i+1); //loop invariant !have_equal_neighbours(a, i); //loop invariant 0 < i ==> a[i-1] != a[i]; */ for (int i = 0; i < n-1; i++) if (a[i] == a[i+1]) return i; return n; } When I compile it with frama-c -jessie -jessie-no-regions -jessie-why-opt="-exp goal" adjacent_find.c then I obtain the error message adjacent_find.c:34:[kernel] user error: Error during annotations analysis: invalid implicit conversion from integer to int which refers to the third loop invariant. I am not sure whether it's a bug or a feature, but when I replace this loop invariant by the following (in my opinion equivalent) loop invariants then most atp can proof all verification conditions. loop invariant !have_equal_neighbours(a, i); loop invariant 0 < i ==> a[i-1] != a[i]; Regards Jens -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100116/476d3b2a/attachment.htm