public class BubbleSort {
    /*@ requires a != null && 0 <= a.length;
      @ ensures (\forall int k; 0 <= k && k < a.length - 1 ==> a[k] <= a[k+1]);
      @*/
    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]);
          @ 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]);
              @ 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;
                }
            }
        }
    }
}