//@+ CheckArithOverflow = no
public class Verif2017SansDoublons {
  /*@ requires 
    @   t.length>0;
    @ ensures 
    @   (\forall integer i; 0< i < t.length && t[i-1] <  t[i])==>\result;
    @*/
  public static boolean tri_sans_doublon(int[] t) {
    /*@ loop_invariant
      @  0 < i  && 
      @  (\forall integer j; 0 < j < i ==> t[j-1] < t[j]);
      @ loop_variant t.length - i - 1; 
      @*/
    for (int i = 1; i < t.length; i++) {
      if (t[i] <= t[i-1])
        return false;
		}
    return true;  
	}		
}