begriffs open source - acsl-example/blob - inc/find1.h

   1 typedef int value_type;
   2 typedef unsigned int size_type;
   3
   4 /*@
   5         requires \valid_read(a + (0..n-1));
   6         assigns \nothing;
   7         ensures 0 <= \result <= n;
   8
   9         behavior some:
  10                 assumes \exists integer i; 0 <= i < n && a[i] == v;
  11                 assigns \nothing;
  12                 ensures 0 <= \result < n;
  13                 ensures a[\result] == v;
  14                 ensures \forall integer i; 0 <= i < \result ==> a[i] != v;
  15
  16         behavior none:
  17                 assumes \forall integer i; 0 <= i < n ==> a[i] != v;
  18                 assigns \nothing;
  19                 ensures \result == n;
  20
  21         complete behaviors;
  22         disjoint behaviors;
  23 */
  24 size_type
  25 find(const value_type* a, size_type n, value_type v);