#include "arrays.pi"

@pre  true
@post sorted(rv, 0, length(a) - 1)
int[] BubbleSort(int[] a)
declare
  int i, j, t;
{
  for
    @(-1 <= i && i < length(a)
      && partitioned(a, 0, i, i + 1, length(a) - 1)
      && sorted(a, i, length(a) - 1))
    (i = length(a) - 1; i > 0; i = i - 1)
  {
    for
      @(1 <= i && i < length(a)
        && 0 <= j && j <= i
        && partitioned(a, 0, i, i + 1, length(a) - 1)
        && partitioned(a, 0, j - 1, j, j)
        && sorted(a, i, length(a) - 1))
      (j = 0; j < i; j = j + 1)
    {
      if (a[j] > a[j + 1]) {
        t = a[j];
        a[j] = a[j + 1];
        a[j + 1] = t;
      }
    }
  }
  return a;
}