package test;

public class InsertionSort {
    /*@ public normal_behavior
      @   requires arr != null;
      @   ensures (\forall int i, j;
      @     0 <= i && i < j && j < arr.length;
      @     arr[i] <= arr[j]);
      @*/
    public static void sort(int[] arr) {
	int i, j, lowest;

	/*@ loop_invariant
	  @   i >= 0 && i <= arr.length &&
	  @   (\forall int j, k;
	  @     0 <= j && j < k && k < i;
	  @     arr[j] <= arr[k]) &&
	  @   (\forall int j, k;
	  @     0 <= j && j < i && k >= i && k < arr.length;
	  @     arr[j] <= arr[k]);
	  @ decreases arr.length - i;
	  @*/
	for (i = 0; i < arr.length; ++i) {
	    lowest = i;

	    /*@ loop_invariant
	      @   j > i && j <= arr.length &&
	      @   lowest >= i && lowest < arr.length &&
	      @   (\forall int k;
	      @     i <= k && k < j;
	      @     arr[lowest] <= arr[k]);
	      @ decreases arr.length - j;
	      @*/
	    for (j = i+1; j < arr.length; ++j)
		if (arr[j] < arr[lowest])
		    lowest = j;

	    int tmp = arr[i];
	    arr[i] = arr[lowest];
	    arr[lowest] = tmp;
	}
    }
}