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

   1 typedef int value_type;
   2 typedef unsigned int size_type;
   3
   4 /*@
   5         axiomatic SomeNone {
   6                 predicate NoneEqual(value_type* a, integer m, integer n, value_type v) =
   7                         \forall integer i; m <= i < n ==> a[i] != v;
   8
   9                 predicate NoneEqual(value_type* a, integer n, value_type v) =
  10                         NoneEqual(a, 0, n, v);
  11         }
  12 */
  13
  14 /*@
  15         axiomatic Find {
  16
  17                 logic integer
  18                 Find(value_type* a, integer m, integer n, value_type v) =
  19                         (n <= m) ?
  20                         0 : ((0 <= Find(a, m, n-1, v) < n-m-1) ?
  21                         Find(a, m, n-1, v) : ((a[n-1] == v) ? n-m-1 : n-m));
  22
  23                 logic integer
  24                 Find(value_type* a, integer n, value_type v) = Find(a, 0, n, v);
  25
  26                 lemma
  27                 Find_Empty:
  28                         \forall value_type *a, v, integer m, n;
  29                         n <= m ==> Find(a, m, n, v) == 0;
  30
  31                 lemma
  32                 Find_Hit:
  33                         \forall value_type *a, v, integer m, n;
  34                         m <= n ==>
  35                         Find(a, m, n, v) < n-m ==>
  36                         Find(a, m, n+1, v) == Find(a, m, n, v);
  37
  38                 lemma
  39                 Find_MissHit:
  40                         \forall value_type *a, v, integer m, n;
  41                         m <= n ==>
  42                         a[n] == v ==>
  43                         Find(a, m, n, v) == n-m ==>
  44                         Find(a, m, n+1, v) == n-m;
  45
  46                 lemma
  47                 Find_MissMiss:
  48                         \forall value_type *a, v, integer m, n;
  49                         m <= n ==>
  50                         a[n] != v ==>
  51                         Find(a, m, n, v) == n-m ==>
  52                         Find(a, m, n+1, v) == (n+1)-m;
  53
  54                 lemma
  55                 Find_Lower:
  56                         \forall value_type *a, v, integer m, n;
  57                         0 <= Find(a, m, n, v);
  58
  59                 lemma
  60                 Find_Upper:
  61                         \forall value_type *a, v, integer m, n;
  62                         m <= n ==> Find(a, m, n, v) <= n-m;
  63
  64                 lemma
  65                 Find_WeaklyIncreasing:
  66                         \forall value_type *a, v, integer m, n;
  67                         m <= n ==> Find(a, m, n, v) <= Find(a, m, n+1, v);
  68
  69                 lemma
  70                 Find_Increasing:
  71                         \forall value_type *a, v, integer k, m, n;
  72                         m <= k <= n ==>
  73                         Find(a, m, k, v) <= Find(a, m, n, v);
  74
  75                 lemma
  76                 Find_Extend:
  77                         \forall value_type *a, v, integer k, m, n;
  78                         m <= k < n ==>
  79                         a[k] == v ==>
  80                         Find(a, m, k, v) == k-m ==>
  81                         Find(a, m, n, v) == k-m;
  82
  83                 lemma
  84                 Find_Limit:
  85                         \forall value_type *a, v, integer k, m, n;
  86                         m <= k < n ==>
  87                         a[k] == v ==>
  88                         Find(a, m, n, v) <= k-m;
  89
  90                 lemma
  91                 Find_NoneEqual:
  92                         \forall value_type *a, v, integer m, n;
  93                         m <= n ==>
  94                         NoneEqual(a, m, n, v) ==>
  95                         Find(a, m, n, v) == n-m;
  96
  97                 lemma
  98                 Find_SomeEqual:
  99                         \forall value_type *a, v, integer k, m, n;
 100                         m <= k < n ==>
 101                         a[k] == v ==>
 102                         NoneEqual(a, m, k, v) ==>
 103                         Find(a, m, n, v) == k-m;
 104
 105                 lemma
 106                 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
 111                 Find_ResultEqual:
 112                         \forall value_type *a, v, integer m, n;
 113                         0 <= Find(a, m, n, v) < n-m ==>
 114                         a[m + Find(a, m, n, v)] == v;
 115         }
 116 */
 117
 118 /*@
 119         requires valid: \valid_read(a + (0..n-1));
 120         assigns         \nothing;
 121         ensures result: 0 <= \result <= n;
 122         ensures result: \result == Find(a, n, v);
 123 */
 124 size_type
 125 find3(const value_type* a, size_type n, value_type v);