public class BubbleSort {
    public static void sort(Node[] a)
    /*:
      requires
        " a ~= null
        & 0 <= Array.length a
        & (ALL k. (0 <= k & k < Array.length a) --> a.[k] ~= null)
        "
      modifies "Array.arrayState"
      ensures
        " (ALL k. (0 <= k & k < Array.length a - 1)
           --> (a.[k]..Node.key <= a.[k+1]..Node.key))
        & (ALL k. (0 <= k & k < Array.length a)
           --> (EX l. 0 <= l & l < Array.length a & a.[k]=old(a.[l])))
        & (ALL k. (0 <= k & k < Array.length a)
           --> (EX l. 0 <= l & l < Array.length a & a.[l]=old(a.[k])))
        & (ALL a1 k. (a1 ~= a) --> a1.[k]=old(a1.[k]))
        "
    */
    {
        if (a.length == 0) return;

        int i = 0;
        while
            /*: inv
              " 0 <= i & i <= Array.length a - 1
              & (ALL k. (0 <= k & k < i - 1) --> a.[k]..Node.key <= a.[k+1]..Node.key)
              & (ALL k l. (0 <= k & k < i & i <= l & l < Array.length a)
                 --> a.[k]..Node.key <= a.[l]..Node.key)
              & (ALL k. (0 <= k & k < Array.length a)
                 --> (EX l. 0 <= l & l < Array.length a & a.[k]=old(a.[l])))
              & (ALL k. (0 <= k & k < Array.length a)
                 --> (EX l. 0 <= l & l < Array.length a & a.[l]=old(a.[k])))
              & (ALL a1 k. (a1 ~= a) --> a1.[k]=old(a1.[k]))
              "
             */
            (i < a.length - 1)
        {
            int j = a.length - 1;
            while
                /*: inv
                  " i <= j & j <= Array.length a - 1
                  & (ALL k. (j < k & k < Array.length a) --> a.[j]..Node.key <= a.[k]..Node.key)
                  & (ALL k. (0 <= k & k < i - 1) --> a.[k]..Node.key <= a.[k+1]..Node.key)
                  & (ALL k l. (0 <= k & k < i & i <= l & l < Array.length a)
                     --> (a.[k]..Node.key <= a.[l]..Node.key))
                  & (ALL k. (0 <= k & k < Array.length a)
                     --> (EX l. 0 <= l & l < Array.length a & a.[k]=old(a.[l])))
                  & (ALL k. (0 <= k & k < Array.length a)
                     --> (EX l. 0 <= l & l < Array.length a & a.[l]=old(a.[k])))
                  & (ALL a1 k. (a1 ~= a) --> a1.[k]=old(a1.[k]))
                  "
                 */
                (j > i)
            {
                if(a[j].key < a[j-1].key) {
                    Node t = a[j];
                    a[j] = a[j-1];
                    a[j-1] = t;
                }
                j = j - 1;
            }
            i = i + 1;
        }
    }
}