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

   1 #ifndef SEARCH_H
   2 #define SEARCH_H
   3
   4 #include "existence.h"
   5
   6 /*@
   7         axiomatic Find {
   8
   9                 logic integer
  10                 Find(value_type* a, integer m, integer n, value_type v) =
  11                         (n <= m) ?
  12                         0 : ((0 <= Find(a, m, n-1, v) < n-m-1) ?
  13                         Find(a, m, n-1, v) : ((a[n-1] == v) ? n-m-1 : n-m));
  14
  15                 logic integer
  16                 Find(value_type* a, integer n, value_type v) = Find(a, 0, n, v);
  17
  18                 lemma
  19                 Find_Empty:
  20                         \forall value_type *a, v, integer m, n;
  21                         n <= m ==> Find(a, m, n, v) == 0;
  22
  23                 lemma
  24                 Find_Hit:
  25                         \forall value_type *a, v, integer m, n;
  26                         m <= n ==>
  27                         Find(a, m, n, v) < n-m ==>
  28                         Find(a, m, n+1, v) == Find(a, m, n, v);
  29
  30                 lemma
  31                 Find_MissHit:
  32                         \forall value_type *a, v, integer m, n;
  33                         m <= n ==>
  34                         a[n] == v ==>
  35                         Find(a, m, n, v) == n-m ==>
  36                         Find(a, m, n+1, v) == n-m;
  37
  38                 lemma
  39                 Find_MissMiss:
  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+1)-m;
  45
  46                 lemma
  47                 Find_Lower:
  48                         \forall value_type *a, v, integer m, n;
  49                         0 <= Find(a, m, n, v);
  50
  51                 lemma
  52                 Find_Upper:
  53                         \forall value_type *a, v, integer m, n;
  54                         m <= n ==> Find(a, m, n, v) <= n-m;
  55
  56                 lemma
  57                 Find_WeaklyIncreasing:
  58                         \forall value_type *a, v, integer m, n;
  59                         m <= n ==> Find(a, m, n, v) <= Find(a, m, n+1, v);
  60
  61                 lemma
  62                 Find_Increasing:
  63                         \forall value_type *a, v, integer k, m, n;
  64                         m <= k <= n ==>
  65                         Find(a, m, k, v) <= Find(a, m, n, v);
  66
  67                 lemma
  68                 Find_Extend:
  69                         \forall value_type *a, v, integer k, m, n;
  70                         m <= k < n ==>
  71                         a[k] == v ==>
  72                         Find(a, m, k, v) == k-m ==>
  73                         Find(a, m, n, v) == k-m;
  74
  75                 lemma
  76                 Find_Limit:
  77                         \forall value_type *a, v, integer k, m, n;
  78                         m <= k < n ==>
  79                         a[k] == v ==>
  80                         Find(a, m, n, v) <= k-m;
  81
  82                 lemma
  83                 Find_NoneEqual:
  84                         \forall value_type *a, v, integer m, n;
  85                         m <= n ==>
  86                         NoneEqual(a, m, n, v) ==>
  87                         Find(a, m, n, v) == n-m;
  88
  89                 lemma
  90                 Find_SomeEqual:
  91                         \forall value_type *a, v, integer k, m, n;
  92                         m <= k < n ==>
  93                         a[k] == v ==>
  94                         NoneEqual(a, m, k, v) ==>
  95                         Find(a, m, n, v) == k-m;
  96
  97                 lemma
  98                 Find_ResultNoneEqual:
  99                         \forall value_type *a, v, integer m, n;
 100                         m <= n ==> NoneEqual(a, m, m + Find(a, m, n, v), v);
 101
 102                 lemma
 103                 Find_ResultEqual:
 104                         \forall value_type *a, v, integer m, n;
 105                         0 <= Find(a, m, n, v) < n-m ==>
 106                         a[m + Find(a, m, n, v)] == v;
 107         }
 108 */
 109
 110 #endif