class Minimum {
    /*@ public normal_behaviour
      @  requires arr != null && arr.length > 0;
      @  ensures (\exists int k; 0 <= k && k < arr.length; 
      @                     \result == arr[k]);
      @  ensures (\exists int k; 0 <= k && k < arr.length; 
      @                     \result >= arr[k]);
      @ also
      @ public exceptional_behaviour
      @  requires arr == null;
      @  signals_only NullPointerException;
      @ also
      @ public exceptional_behaviour
      @  requires arr != null && arr.length == 0;
      @  signals_only ArrayIndexOutOfBoundsException;
      @*/
    int min(/*@nullable@*/ int[] arr) {
	int min = arr[0];
	/*@
	  @ loop_invariant (\exists int k; 0 <= k && k < i; arr[k] == min);
	  @ loop_invariant 0 <= i && i <= arr.length;
	  @ loop_invariant (\forall int l; 0 <= l && l < i; arr[l] >= min);
	  @ modifies i, min;
	  @ decreases arr.length - i;
	  @*/
	for (int i = 1; i < arr.length; i++) {
	    if (arr[i] < min)
		min = arr[i];
	}
	return min;
    }
}