C0

// Binary search implementation in C0
// Returns index of target in sorted array, or -1 if not found

int binary_search(int[] arr, int target)
//@requires \length(arr) >= 0;
//@requires is_sorted(arr, 0, \length(arr));
{
  int left = 0;
  int right = \length(arr) - 1;

  while (left <= right) {
    int mid = left + (right - left) / 2;

    if (arr[mid] == target) {
      return mid;
    } else if (arr[mid] < target) {
      left = mid + 1;
    } else {
      right = mid - 1;
    }
  }

  return -1;
}

bool is_sorted(int[] arr, int lo, int hi)
//@requires 0 <= lo && lo <= hi && hi <= \length(arr);
{
  for (int i = lo; i < hi - 1; i++)
  //@loop_invariant lo <= i;
  {
    if (arr[i] > arr[i + 1]) return false;
  }
  return true;
}

int main() {
  int[] arr = alloc_array(int, 7);
  arr[0] = 1;
  arr[1] = 3;
  arr[2] = 5;
  arr[3] = 7;
  arr[4] = 9;
  arr[5] = 11;
  arr[6] = 13;

  int result = binary_search(arr, 7);
  return result;
}