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

   1 #include "find1.h"
   2
   3 size_type
   4 find(const value_type* a, size_type n, value_type v)
   5 {
   6         /*@
   7           loop invariant 0 <= i <= n;
   8           loop invariant \forall integer k; 0 <= k < i ==> a[k] != v;
   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                         return i;
  15                 }
  16         }
  17         return n;
  18 }