Bubble sort as in Sedgewick

module BubbleSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

  let bubble_sort (a: array int) =
    ensures { sorted a }
'L:
    for i = length a downto 2 do
      invariant { sorted_sub a i (length a) }
      invariant { forall k: int. forall k': int. 0 <= k < i -> i <= k' < length a
          -> a[k] <= a[k'] }
'L1:    for j = 1 to i-1 do
        invariant { forall k: int. 0 <= k < j-1 -> a[k] <= a[j-1] }
	invariant { array_eq_sub (at a 'L1) a i (length a) }
        invariant { permut_sub (at a 'L1) a 0 i }
'L2:
        if a[j-1] > a[j] then begin
          let t = a[j] in a[j] <- a[j-1]; a[j-1] <- t;
          assert { exchange (at a 'L2) a (j - 1) j }
        end
      done
    done

end