predicate sorted(a: array<int>, lo: int, hi: int)
requires a != null;
requires 0 <= lo <= hi <= a.Length;
reads a;
{forall j,k :: lo <= j < k < hi ==> a[j] <= a[k]}

method sort (a: array<int>)
requires a != null
ensures sorted(a, 0, a.Length)
modifies a;
{
	if a.Length <= 1 { return; }
	var i: int := 1;
	while i < a.Length
	decreases a.Length - i
	invariant 1 <= i <= a.Length && sorted(a, 0, i)
	{
		var j: int := i;
		while j > 0 && a[j] < a[j-1]
		decreases j
		invariant 0 <= j <= i && sorted(a, 0, j) && sorted(a,j,i+1) && (0 < j < i) ==> a[j-1] <= a[j+1]
		{
			a[j], a[j-1] := a[j-1], a[j];
			j := j-1;
		}
		i := i+1;
	}
}