bubbleSort.gcl

-- Bubble sort.
-- `n` is an experiment parameter; replace it with a concrete value.

bubbleSort(n: Int, a: [Int]) -> b: [Int] {
  assume #a >= 0 && #a >= n;

  let k: Int {
    k = 0;

    -- inv of outer loop
    assert 0 <= k && k <= #a &&
      forall i. 0 <= i && i < k =>
        forall j. i <= j && j < #a => a[i] <= a[j];

    while k < #a {
      let m: Int, tmp: Int {
        m = #a - 1;

        -- inv of inner loop
        assert
          0 <= k && k <= #a
          && (forall i. 0 <= i && i < k => forall j. i <= j && j < #a => a[i] <= a[j])
          && k <= m && m < #a
          && forall j. m <= j && j < #a => a[m] <= a[j];

        while k < m {
          if a[m] < a[m - 1] {
            tmp = a[m];
            a[m] = a[m - 1];
            a[m - 1] = tmp;
          }

          m = m - 1;
        }
      }

      k = k + 1;
    }
  }

  b = a;
  assert forall i. 0 <= i && i < #b => forall j. i <= j && j < #b => b[i] <= b[j];
}