begriffs open source - acsl-example/blob - src/find3.c

   1 #include "find3.h"
   2
   3 size_type
   4 find3(const value_type* a, size_type n, value_type v)
   5 {
   6         /*@
   7           loop invariant bound: 0 <= i <= n;
   8           loop invariant not_found: Find(a, i, v) == i;
   9           loop assigns i;
  10           loop variant n-i;
  11           */
  12         for (size_type i = 0u; i < n; i++) {
  13                 if (a[i] == v) {
  14                         //@ assert found: Find(a, n, v) == i;
  15                         return i;
  16                 }
  17         }
  18         return n;
  19 }