#include "arrays.pi"

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