/*@ axiomatic NumOf {
  @  logic integer num_of{L}(int e, integer i, integer j, int t[]);
  @  axiom num_of_empty_case{L} :
  @   \forall int e, integer i j, int t[];
  @    i > j ==> num_of(e, i,j,t) == 0;
  @  axiom num_of_true_case{L} :
  @   \forall int e, integer i j k, int t[];
  @       i <= j && t[j] == e ==> 
  @         num_of(e,i,j,t) == num_of(e,i,j-1,t) + 1;
  @  axiom num_of_false_case{L} :
  @   \forall int e, integer i j k, int t[];
  @       i <= j && ! (t[j] == e) ==> 
  @         num_of(e,i,j,t) == num_of(e,i,j-1,t);
  @ }
  @*/

public class BubbleSort3 {
    /*@ requires a != null;
      @ assigns a[..];
      @ ensures (\forall int k; 0 <= k && k < a.length - 1 ==> a[k] <= a[k+1])
      @      && (\forall int k; (0 <= k && k < a.length)
      @          ==> (\exists int l; 0 <= l && l < a.length && a[k]==\old(a[l])))
      @      && (\forall int k; (0 <= k && k < a.length)
      @          ==> (\exists int l; 0 <= l && l < a.length && a[l]==\old(a[k])))
      @      && (\forall int e; num_of(e, 0, a.length-1, a)==\old(num_of(e, 0, a.length-1, a)));
      @*/
    public static void sort(int[] a)
    {
        if (a.length == 0) return;

        /*@ loop_invariant
          @   0 <= i && i <= a.length - 1 && 
          @   (\forall int k; 0 <= k && k < i - 1 ==> a[k] <= a[k+1]) &&
          @   (\forall int k l; 0 <= k && k < i && i <= l && l < a.length ==> a[k] <= a[l]) &&
          @   (\forall int k; (0 <= k && k < a.length)
          @    ==> (\exists int l; 0 <= l && l < a.length && a[k]==\at(a[l], Pre))) &&
          @   (\forall int k; (0 <= k && k < a.length)
          @    ==> (\exists int l; 0 <= l && l < a.length && a[l]==\at(a[k], Pre))) &&
          @   (\forall int e; num_of(e, 0, a.length-1, a)==\at(num_of(e, 0, a.length-1, a), Pre));
          @ loop_variant a.length - 1 - i;
          @*/
        for (int i = 0; i < a.length - 1; i++) {

            /*@ loop_invariant
              @   i <= j && j <= a.length - 1 && 
              @   (\forall int k; j < k && k < a.length ==> a[j] <= a[k]) &&
              @   (\forall int k; 0 <= k && k < i - 1 ==> a[k] <= a[k+1]) &&
              @   (\forall int k l; 0 <= k && k < i && i <= l && l < a.length ==> a[k] <= a[l]) &&
              @   (\forall int k; (0 <= k && k < a.length)
              @    ==> (\exists int l; 0 <= l && l < a.length && a[k]==\at(a[l], Pre))) &&
              @   (\forall int k; (0 <= k && k < a.length)
              @    ==> (\exists int l; 0 <= l && l < a.length && a[l]==\at(a[k], Pre))) &&
              @   (\forall int e; num_of(e, 0, a.length-1, a)==\at(num_of(e, 0, a.length-1, a), Pre));
              @ loop_variant j - i;
              @*/
            for (int j = a.length - 1; j > i; j--) {
                if(a[j] < a[j-1]) {
                    int t = a[j];
                    a[j] = a[j-1];
                    a[j-1] = t;
                }
            }
        }
    }
}