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

   1 #include "find.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 }
  19
  20 size_type
  21 find2(const value_type* a, size_type n, value_type v)
  22 {
  23         /*@
  24           loop invariant bound:     0 <= i <= n;
  25           loop invariant not_found: NoneEqual(a, i, v);
  26           loop assigns i;
  27           loop variant n-i;
  28           */
  29         for (size_type i = 0u; i < n; i++) {
  30                 if (a[i] == v) {
  31                         return i;
  32                 }
  33         }
  34         return n;
  35 }
  36
  37 size_type
  38 find3(const value_type* a, size_type n, value_type v)
  39 {
  40         /*@
  41           loop invariant bound: 0 <= i <= n;
  42           loop invariant not_found: Find(a, i, v) == i;
  43           loop assigns i;
  44           loop variant n-i;
  45           */
  46         for (size_type i = 0u; i < n; i++) {
  47                 if (a[i] == v) {
  48                         //@ assert found: Find(a, n, v) == i;
  49                         return i;
  50                 }
  51         }
  52         return n;
  53 }