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

   1 #ifndef EXISTENCE_H
   2 #define EXISTENCE_H
   3
   4 #include "types.h"
   5
   6 /*@
   7         axiomatic SomeNone {
   8                 predicate SomeEqual{A}(value_type* a, integer m, integer n, value_type v) =
   9                         \exists integer i; m <= i < n && a[i] == v;
  10
  11                 predicate SomeEqual{A}(value_type* a, integer n, value_type v) =
  12                         SomeEqual(a, 0, n, v);
  13
  14                 predicate NoneEqual(value_type* a, integer m, integer n, value_type v) =
  15                         \forall integer i; m <= i < n ==> a[i] != v;
  16
  17                 predicate NoneEqual(value_type* a, integer n, value_type v) =
  18                         NoneEqual(a, 0, n, v);
  19
  20                 lemma
  21                 NotSomeEqual_NoneEqual:
  22                         \forall value_type *a, v, integer m, n;
  23                         !SomeEqual(a, m, n, v) ==> NoneEqual(a, m, n, v);
  24
  25                 lemma
  26                 NoneEqual_NotSomeEqual:
  27                         \forall value_type *a, v, integer m, n;
  28                         NoneEqual(a, m, n, v) ==> !SomeEqual(a, m, n, v);
  29         }
  30 */
  31
  32 #endif