--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] adjacent_find problem



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