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

   1 #include "algos.h"
   2
   3 /*@
   4         requires \valid_read(a + (0..n-1));
   5         assigns \nothing;
   6         ensures 0 <= \result <= n;
   7
   8         behavior some:
   9                 assumes \exists integer i; 0 <= i < n && a[i] == v;
  10                 assigns \nothing;
  11                 ensures 0 <= \result < n;
  12                 ensures a[\result] == v;
  13                 ensures \forall integer i; 0 <= i < \result ==> a[i] != v;
  14
  15         behavior none:
  16                 assumes \forall integer i; 0 <= i < n ==> a[i] != v;
  17                 assigns \nothing;
  18                 ensures \result == n;
  19
  20         complete behaviors;
  21         disjoint behaviors;
  22 */
  23 size_type
  24 find(const value_type* a, size_type n, value_type v)
  25 {
  26         /*@
  27           loop invariant 0 <= i <= n;
  28           loop invariant \forall integer k; 0 <= k < i ==> a[k] != v;
  29           loop assigns i;
  30           loop variant n-i;
  31           */
  32         for (size_type i = 0u; i < n; i++) {
  33                 if (a[i] == v) {
  34                         return i;
  35                 }
  36         }
  37         return n;
  38 }