public class BubbleSort2 {
    /*@ 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])));
      @*/
    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)));
          @ 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)));
              @ 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;
                }
            }
        }
    }
}