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

   1 typedef int value_type;
   2 typedef unsigned int size_type;
   3
   4 /*@
   5         axiomatic SomeNone {
   6                 predicate SomeEqual{A}(value_type* a, integer m, integer n, value_type v) =
   7                         \exists integer i; m <= i < n && a[i] == v;
   8
   9                 predicate SomeEqual{A}(value_type* a, integer n, value_type v) =
  10                         SomeEqual(a, 0, n, v);
  11
  12                 predicate NoneEqual(value_type* a, integer m, integer n, value_type v) =
  13                         \forall integer i; m <= i < n ==> a[i] != v;
  14
  15                 predicate NoneEqual(value_type* a, integer n, value_type v) =
  16                         NoneEqual(a, 0, n, v);
  17
  18                 lemma
  19                 NotSomeEqual_NoneEqual:
  20                         \forall value_type *a, v, integer m, n;
  21                         !SomeEqual(a, m, n, v) ==> NoneEqual(a, m, n, v);
  22
  23                 lemma
  24                 NoneEqual_NotSomeEqual:
  25                         \forall value_type *a, v, integer m, n;
  26                         NoneEqual(a, m, n, v) ==> !SomeEqual(a, m, n, v);
  27         }
  28 */
  29
  30 /*@
  31         requires valid: \valid_read(a + (0..n-1));
  32         assigns \nothing;
  33         ensures result: 0 <= \result <= n;
  34
  35         behavior some:
  36                 assumes         SomeEqual(a, n, v);
  37                 assigns         \nothing;
  38                 ensures bound:  0 <= \result < n;
  39                 ensures result: a[\result] == v;
  40                 ensures first:  NoneEqual(a, \result, v);
  41
  42         behavior none:
  43                 assumes         NoneEqual(a, n, v);
  44                 assigns         \nothing;
  45                 ensures result: \result == n;
  46
  47         complete behaviors;
  48         disjoint behaviors;
  49 */
  50 size_type
  51 find2(const value_type* a, size_type n, value_type v);