class InsertionSort {
   /*@ requires arr != null && arr.length > 0;
     @ ensures (\forall int m; m >= 1 && m < arr.length; 
     @             arr[m] >= arr[m-1]); @*/ 
   public static void sort(int[] arr) {
       int i,j;
       /*@ loop_invariant (\forall int l; l < i && l >= 1; arr[l] >= arr[l-1]);
	 @ loop_invariant i >= 1 && i <= arr.length;
	 @ assignable i,j,arr[*];
	 @ decreases arr.length - i;
	 @*/
      for(i = 1; i < arr.length; i++) {
	  /*@ loop_invariant j < arr.length;
	    @ loop_invariant (\forall int k; 0 < k && k <= i;
	    @                    k == j || arr[k] >= arr[k - 1]);
	    @ loop_invariant (0 < j && j < i ==> arr[j+1] >= arr[j-1]);
	    @ loop_invariant j <= i && j >= 0;
	    @ assignable j,arr[*];
	    @ decreases j;
	    @*/
         for(j = i; j > 0; j--) {
            if (arr[j] <= arr[j-1]) {
               int tmp = arr[j];
               arr[j] = arr[j-1];
               arr[j-1] = tmp;
            }
         }
      }
   }
}