// ============================================================================
// Name:        BinarySearch
// Description: Find an element in a sorted array of numbers.
// References:  T.H. Cormen, C.E. Leiserson, R.L. Rivest. Introduction to
//              Algorithms. MIT Press, 1997.
//              R. Sedgewick. Algorithms. Addison-Wesley, 1991.
//              http://en.wikipedia.org/wiki/Binary_search
// Parameters:  SIZE (size of array)
//              INFINITE (use variables with infinite bit width)
//              BITS (bit width for finite variables)
// ============================================================================

#ifndef SIZE
#define SIZE 4u
#endif

#ifdef INFINITE
#define TYPE int
#else
#ifndef BITS
#define BITS 4u
#endif
#define TYPE int[BITS]
#endif

#define SORTED(a) (forall(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-2u)) a[i] <= a[i+1u])
#define CONTAINS(a,x) (exists(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u)) x == a[i])

module BinarySearch(TYPE z, b[SIZE], &a[SIZE], &value, nat[sizeOf(SIZE-1u)] &left, &right, &mid, event &ready)
   implements SearchSpec(a, value, left, ready) {
   sequence(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
      a[i] = b[i];

   value = z;
   left = 0u;
   right = SIZE-1u;

   do {
      mid = (left+right)/2u;
      if(value <= a[mid])
         next(right) = mid;
      else
         next(left) = mid+1u;
      pause;
   } while(left<right);

   emit ready;
}

spec SearchSpec(TYPE a[SIZE], value, nat[sizeOf(SIZE-1u)] left, bool ready) {
   termination: SORTED(a) -> A F ready;
   correctness: SORTED(a) & CONTAINS(a,value) -> A G (ready -> (a[left] == value));
   finalInterval: A G (ready -> left == right);
}