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 { permut_all (old a) a }
'L:
    for i = length a downto 2 do
      invariant { permut_all (at a 'L) a }
'L1:    for j = 1 to i-1 do
        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 };
          assert { permut_sub (at a 'L2) a 0 i }
        end
      done
    done

end