#include "arrays.pi"

@pre  true
@post sorted(rv, 0, length(a) - 1)
int[] BubbleSort(int[] a)
declare
  int i, j, t;
{
  for
    @ true
    (i = length(a) - 1; i > 0; i = i - 1)
  {
    for
      @ true
      (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;
}