begriffs open source - acsl-example/blob - inc/find.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 NotSomeEqual_NoneEqual:
  19                         \forall value_type *a, v, integer m, n;
  20                         !SomeEqual(a, m, n, v) ==> NoneEqual(a, m, n, v);
  21
  22                 lemma NoneEqual_NotSomeEqual:
  23                         \forall value_type *a, v, integer m, n;
  24                         NoneEqual(a, m, n, v) ==> !SomeEqual(a, m, n, v);
  25         }
  26 */
  27
  28 /*@
  29         axiomatic Find {
  30                 logic integer
  31                 Find(value_type* a, integer m, integer n, value_type v) =
  32                         (n <= m) ?
  33                         0 : ((0 <= Find(a, m, n-1, v) < n-m-1) ?
  34                         Find(a, m, n-1, v) : ((a[n-1] == v) ? n-m-1 : n-m));
  35
  36                 logic integer
  37                 Find(value_type* a, integer n, value_type v) = Find(a, 0, n, v);
  38
  39                 lemma Find_Empty:
  40                         \forall value_type *a, v, integer m, n;
  41                         n <= m ==> Find(a, m, n, v) == 0;
  42
  43                 lemma Find_Hit:
  44                         \forall value_type *a, v, integer m, n;
  45                         m <= n ==>
  46                         Find(a, m, n, v) < n-m ==>
  47                         Find(a, m, n+1, v) == Find(a, m, n, v);
  48
  49                 lemma Find_MissHit:
  50                         \forall value_type *a, v, integer m, n;
  51                         m <= n ==>
  52                         a[n] == v ==>
  53                         Find(a, m, n, v) == n-m ==>
  54                         Find(a, m, n+1, v) == n-m;
  55
  56                 lemma Find_MissMiss:
  57                         \forall value_type *a, v, integer m, n;
  58                         m <= n ==>
  59                         a[n] != v ==>
  60                         Find(a, m, n, v) == n-m ==>
  61                         Find(a, m, n+1, v) == (n+1)-m;
  62
  63                 lemma Find_Lower:
  64                         \forall value_type *a, v, integer m, n;
  65                         0 <= Find(a, m, n, v);
  66
  67                 lemma Find_Upper:
  68                         \forall value_type *a, v, integer m, n;
  69                         m <= n ==> Find(a, m, n, v) <= n-m;
  70
  71                 lemma Find_WeaklyIncreasing:
  72                         \forall value_type *a, v, integer m, n;
  73                         m <= n ==> Find(a, m, n, v) <= Find(a, m, n+1, v);
  74
  75                 lemma Find_Increasing:
  76                         \forall value_type *a, v, integer k, m, n;
  77                         m <= k <= n ==>
  78                         Find(a, m, k, v) <= Find(a, m, n, v);
  79
  80                 lemma Find_Extend:
  81                         \forall value_type *a, v, integer k, m, n;
  82                         m <= k < n ==>
  83                         a[k] == v ==>
  84                         Find(a, m, k, v) == k-m ==>
  85                         Find(a, m, n, v) == k-m;
  86
  87                 lemma Find_Limit:
  88                         \forall value_type *a, v, integer k, m, n;
  89                         m <= k < n ==>
  90                         a[k] == v ==>
  91                         Find(a, m, n, v) <= k-m;
  92
  93                 lemma Find_NoneEqual:
  94                         \forall value_type *a, v, integer m, n;
  95                         m <= n ==>
  96                         NoneEqual(a, m, n, v) ==>
  97                         Find(a, m, n, v) == n-m;
  98
  99                 lemma Find_SomeEqual:
 100                         \forall value_type *a, v, integer k, m, n;
 101                         m <= k < n ==>
 102                         a[k] == v ==>
 103                         NoneEqual(a, m, k, v) ==>
 104                         Find(a, m, n, v) == k-m;
 105
 106                 lemma Find_ResultNoneEqual:
 107                         \forall value_type *a, v, integer m, n;
 108                         m <= n ==> NoneEqual(a, m, m + Find(a, m, n, v), v);
 109
 110                 lemma Find_ResultEqual:
 111                         \forall value_type *a, v, integer m, n;
 112                         0 <= Find(a, m, n, v) < n-m ==>
 113                         a[m + Find(a, m, n, v)] == v;
 114         }
 115 */
 116
 117 /*@
 118         requires \valid_read(a + (0..n-1));
 119         assigns \nothing;
 120         ensures 0 <= \result <= n;
 121
 122         behavior some:
 123                 assumes \exists integer i; 0 <= i < n && a[i] == v;
 124                 assigns \nothing;
 125                 ensures 0 <= \result < n;
 126                 ensures a[\result] == v;
 127                 ensures \forall integer i; 0 <= i < \result ==> a[i] != v;
 128
 129         behavior none:
 130                 assumes \forall integer i; 0 <= i < n ==> a[i] != v;
 131                 assigns \nothing;
 132                 ensures \result == n;
 133
 134         complete behaviors;
 135         disjoint behaviors;
 136 */
 137 size_type
 138 find(const value_type* a, size_type n, value_type v);
 139
 140 /*@
 141         requires valid: \valid_read(a + (0..n-1));
 142         assigns \nothing;
 143         ensures result: 0 <= \result <= n;
 144
 145         behavior some:
 146                 assumes         SomeEqual(a, n, v);
 147                 assigns         \nothing;
 148                 ensures bound:  0 <= \result < n;
 149                 ensures result: a[\result] == v;
 150                 ensures first:  NoneEqual(a, \result, v);
 151
 152         behavior none:
 153                 assumes         NoneEqual(a, n, v);
 154                 assigns         \nothing;
 155                 ensures result: \result == n;
 156
 157         complete behaviors;
 158         disjoint behaviors;
 159 */
 160 size_type
 161 find2(const value_type* a, size_type n, value_type v);
 162
 163 /*@
 164         requires valid: \valid_read(a + (0..n-1));
 165         assigns         \nothing;
 166         ensures result: 0 <= \result <= n;
 167         ensures result: \result == Find(a, n, v);
 168 */
 169 size_type
 170 find3(const value_type* a, size_type n, value_type v);