import java.util.Arrays;
import java.util.Random;

public class BinarySearch
{

  /*@
    @ requires a != null;
    @ requires (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
    @ ensures \result >= 0;
    @ ensures \result <= a.length;
    @ ensures (\forall int i; i >= 0 && i < \result; a[i] < item);
    @ ensures (\forall int i; i >= \result && i < a.length; item <= a[i]);
    @ ensures (\exists int i; i >= 0 && i < a.length; a[i] == item) ==>
    @          a[\result] == item;
    @*/
  public static int binarySearch(final int[] a, final int item)
  {
    int lower = 0;
    int upper = a.length;
    while (lower < upper) {
      final int mid = (upper + lower) / 2;
      if (item <= a[mid]) {
        upper = mid;
      } else {
        lower = mid + 1;
      }
    }
    return lower;
  }


  /*@
    @ requires args != null;
    @*/
  public static void main(final String[] args)
    throws RuntimeException
  {
    if (args.length != 1) {
      System.err.println
        ("USAGE: jmlrac " + BinarySearch.class.getName() + " <number>");
      return;
    }
    final Random random = new Random();
    final int number = Integer.parseInt(args[0]);
    if (number <= 0) {
      System.err.println("Number of tries must be greater than 0!");
      return;
    }
    final int max = number / 2;
    final int[] a = new int[number];
    for (int i = 0; i < number; i++) {
      a[i] = random.nextInt(max);
    }
    Arrays.sort(a);
    for (int i = 0; i < number; i++) {
      final int item = random.nextInt(number);
      binarySearch(a, item);
    }
  }
      
}