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

   1 #include "proof/search.h"
   2 #include "algos.h"
   3
   4 /*@
   5         requires valid: \valid_read(a + (0..n-1));
   6         assigns         \nothing;
   7         ensures result: 0 <= \result <= n;
   8         ensures result: \result == Find(a, n, v);
   9 */
  10 size_type
  11 find3(const value_type* a, size_type n, value_type v)
  12 {
  13         /*@
  14           loop invariant bound: 0 <= i <= n;
  15           loop invariant not_found: Find(a, i, v) == i;
  16           loop assigns i;
  17           loop variant n-i;
  18           */
  19         for (size_type i = 0u; i < n; i++) {
  20                 if (a[i] == v) {
  21                         //@ assert found: Find(a, n, v) == i;
  22                         return i;
  23                 }
  24         }
  25         return n;
  26 }