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

   1 #include "proof/existence.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
   9         behavior some:
  10                 assumes         SomeEqual(a, n, v);
  11                 assigns         \nothing;
  12                 ensures bound:  0 <= \result < n;
  13                 ensures result: a[\result] == v;
  14                 ensures first:  NoneEqual(a, \result, v);
  15
  16         behavior none:
  17                 assumes         NoneEqual(a, n, v);
  18                 assigns         \nothing;
  19                 ensures result: \result == n;
  20
  21         complete behaviors;
  22         disjoint behaviors;
  23 */
  24 size_type
  25 find2(const value_type* a, size_type n, value_type v)
  26 {
  27         /*@
  28           loop invariant bound:     0 <= i <= n;
  29           loop invariant not_found: NoneEqual(a, i, v);
  30           loop assigns i;
  31           loop variant n-i;
  32           */
  33         for (size_type i = 0u; i < n; i++) {
  34                 if (a[i] == v) {
  35                         return i;
  36                 }
  37         }
  38         return n;
  39 }