//@+ CheckArithOverflow = no
public class TPWhy {

  /*@ ensures \result >= x && \result >= y &&
    @   \forall integer z; z >= x && z >= y ==> z >= \result;
    @*/
  public static int max(int x, int y) {
    if (x>y)
      return x; 
    else 
      return y;
  }

  /*@ requires t != null && t.length >= 1;
    @ ensures
    @   0 <= \result < t.length &&
    @   \forall integer i; 0 <= i < t.length ==> t[i] <= t[\result];
    @*/
  public static int findMax(int[] t) {
    int m = t[0];
    int r = 0;
    /*@ loop_invariant
      @   1 <= i <= t.length && 0 <= r < t.length &&
      @   m == t[r] && \forall integer j; 0 <= j < i ==> t[j] <= t[r];
      @ loop_variant t.length - i;
      @*/
    for (int i=1; i < t.length; i++) {
      if (t[i] > m) {
        r = i;
        m = t[i];
      }
    }
    return r;
  } 

  /*@ requires t != null;
    @ ensures
    @   \result <==> (\forall integer i; 0 <= i < t.length ==> t[i] == 0);
    @*/
  public static boolean allZeros(int[] t) {
    boolean r = true;
    int i = 0;
    /*@ loop_invariant
      @   0 <= i <= t.length && \forall integer j; 0 <= j < i ==> t[j] == 0;
      @ loop_variant t.length - i;
      @*/
    while (i < t.length && t[i] == 0) {
      i = i + 1;
    }
    if (i < t.length) {
      r = false;
    }
    return r;
  }

  /*@ requires n >= 0;
    @ ensures \result == n * n;
    @*/
  public static int square(int n) {
    int cpt = n;
    int r = 0;
    /*@ loop_invariant
      @   r == n*n - cpt*n && cpt >= 0;
      @ loop_variant cpt;
      @*/
    while (cpt > 0) {
      r = r + n;
      cpt = cpt - 1;
    }
    return r;
  }

  /*@ requires n >= 0;
    @ ensures
    @   \result >= 0 && \result * \result <= n
    @   && n < (\result + 1) * (\result + 1);
    @*/
  public static int sqrt(int n) {
    int r = 0;
    /*@ loop_invariant r >= 0 && n >= r*r;
      @ loop_variant n - r*r;
      @*/
    while (n >= (r+1)*(r+1)) {
      r = r + 1;
    }
    return r;
  }

  /*@ requires x >= y >= 0;
    @ ensures \result == x * y;
    @*/
  public int mult(int x, int y) {
    int r = 0;
    int a = x;
    int b = y;
    /*@ loop_invariant r + a * b == x * y && a >= b >= 0;
      @ loop_variant b;
      @*/
    while (b > 0) {
      if (b % 2 == 1) {
        r = r + a;
      }
      a = 2 * a;
      b = b / 2;
    }
    return r;
  }

}