Verifying QuickSort in Boogie

sv_boogie.bpl

const N: int;
axiom 1 < N;
var a: [int]int;
var perm: [int]int;

procedure __new_perm__() returns (perm: [int]int)
	ensures perm_ok(perm);
	ensures (forall k: int :: 0 <= k && k < N ==> perm[k] == k);
{
 	var n: int; n := 0;
	while ( n < N )
		invariant (forall k: int :: 0 <= k && k < n ==> perm[k] == k);
	{
		perm[n] := n;
		n := n + 1;
	}
}

/* Check that p is a permutation. */
function perm_ok(perm: [int]int): bool
{
	(forall k: int :: { perm[k] } 0 <= k && k < N ==> 0 <= perm[k] && perm[k] < N)
	&&
	(forall k, l: int :: 0 <= k && k < l && l < N ==> perm[k] != perm[l])
}

/* Check that the first array is the given permutation of the second array. */
function is_perm(A: [int]int, B: [int]int, p: [int]int): bool
{
	(forall k: int :: { A[k] } 0 <= k && k < N ==> A[k] == B[p[k]])
}

function is_monotonic(a: [int]int, low: int, high: int): bool
{
	( forall i, j: int :: low <= i && i <= j && j <= high ==> (a[i] <= a[j]) )
}

procedure partition(p: int, r: int, min: int, max: int) returns (pivot: int, local_perm: [int]int)
	requires 0 <= p && p < r && r < N;
	requires perm_ok(perm);

	requires (forall k: int :: p <= k && k <= r ==> min <= a[k]);
	requires (forall k: int :: p <= k && k <= r ==> a[k] <= max);

	modifies a;
	modifies perm;
	
	ensures pivot <= r;
	ensures p <= pivot;

	ensures (forall k: int ::     p <= k && k < pivot ==> a[k] <= a[pivot]);
	ensures (forall k: int :: pivot <  k && k <= r    ==> a[k] >  a[pivot]);

	ensures perm_ok(perm);
	ensures perm_ok(local_perm);
	ensures is_perm(a, old(a), local_perm);


	ensures (forall k: int :: p <= k && k <= r ==> min <= a[k]);
	ensures (forall k: int :: p <= k && k <= r ==> a[k] <= max);

	ensures (forall k: int :: { a[k] } !(p <= k && k <= r) ==> a[k] == old(a)[k]);

{
	var i, j: int;

	call local_perm := __new_perm__( );

	i := p - 1;
	j := p;

	while ( j < r )
		invariant -1 <= i && i < j && j <= r && r < N;
		invariant p-1 <= i;

		invariant (forall k: int :: p <= k && k <= i ==> a[k] <= a[r]);
		invariant (forall k: int :: i <  k && k <  j ==> a[k] >  a[r]);

		invariant perm_ok(perm);
		invariant perm_ok(local_perm);
		invariant is_perm(a, old(a), local_perm);

		invariant (forall k: int :: p <= k && k <= r ==> min <= a[k]);
		invariant (forall k: int :: p <= k && k <= r ==> a[k] <= max);

		invariant (forall k: int :: { a[k] } !(p <= k && k <= r) ==> a[k] == old(a)[k]);
	{
		if ( a[j] <= a[r] ) {
			i := i + 1;

			call perm := swapElems(i, j);
			
			call local_perm := compose_perm(local_perm, perm);
		}
		j := j + 1;
	}

	call perm := swapElems(i+1, j);
	call local_perm := compose_perm(local_perm, perm);

	pivot := i+1;
}

procedure minMaxElem(lo: int, hi: int) returns (min: int, max: int)
	requires (0 <= lo && lo <= hi && hi < N) || hi < lo;
	ensures (forall k: int :: lo <= k && k <= hi ==> min <= a[k]);
	ensures lo <= hi ==> (exists k: int :: lo <= k && k <= hi && min == a[k]);
	ensures (forall k: int :: lo <= k && k <= hi ==> a[k] <= max);
	ensures lo <= hi ==> (exists k: int :: lo <= k && k <= hi && max == a[k]);
{
	var i: int;
	min := a[lo];
	max := a[lo];
	i := lo+1;
	if ( lo < hi ) {
		while ( i <= hi )
			invariant i <= hi + 1;
			invariant (forall k: int :: lo <= k && k < i ==> min <= a[k]);
			invariant (exists k: int :: lo <= k && k < i && min == a[k]);
			invariant (forall k: int :: lo <= k && k < i ==> a[k] <= max);
			invariant (exists k: int :: lo <= k && k < i && max == a[k]);
		{
			if ( min > a[i] ) {
				min := a[i];
			}
			if ( max < a[i] ) {
				max := a[i];
			}
			i := i + 1;
		}
	}
}

procedure quickSort(p: int, r: int, min: int, max: int) returns (local_perm: [int]int)
	requires (0 <= p && p <= r && r < N) || r < p;

	requires (forall k: int :: p <= k && k <= r ==> min <= a[k]);
	requires (forall k: int :: p <= k && k <= r ==> a[k] <= max);

	requires perm_ok(perm);

	modifies a;
	modifies perm;

	/* TODO: Prove ascending order of the sorted array. */
	
	ensures r <= p ==> (forall k, l: int :: p <= k && k <= l && l <= r ==> a[k] <= a[l]);
	
	ensures (forall k, l: int :: p <= k && k <= l && l <= r ==> a[k] <= a[l]);

	ensures (forall k: int :: { a[k] } p <= k && k <= r ==> min <= a[k]);
	ensures (forall k: int :: { a[k] } p <= k && k <= r ==> a[k] <= max);

	ensures (forall k: int :: { a[k] } !(p <= k && k <= r) ==> a[k] == old(a)[k]);

	ensures perm_ok(perm);
	ensures perm_ok(local_perm);
	ensures is_perm(a, old(a), local_perm);

{
	var q, sub_min, sub_max: int;

	call local_perm := __new_perm__( );
	if ( p < r )
	{
		call q, local_perm := partition(p, r, min, max);

		assert (forall k: int :: { a[k] } p <= k && k <= r ==> min <= a[k]);
		assert (forall k: int :: { a[k] } !(p <= k && k <= r) ==> a[k] == old(a)[k]);

		call sub_min, sub_max := minMaxElem(p, q-1);
		call perm := quickSort(p, q-1, sub_min, sub_max); 
		call local_perm := compose_perm(local_perm, perm);

		call sub_min, sub_max := minMaxElem(q+1, r);
		call perm := quickSort(q+1, r, sub_min, sub_max); 
		call local_perm := compose_perm(local_perm, perm);
	} 
}

procedure compose_perm(old_perm: [int]int, new_perm: [int]int) returns (res_perm: [int]int)
	requires perm_ok(old_perm);
	requires perm_ok(new_perm);
	ensures perm_ok(res_perm);
	ensures (forall k: int :: 0 <= k && k < N ==> res_perm[k] == old_perm[ new_perm[k] ]);
{
	var i: int;
	i := 0;
	while ( i < N )
		invariant i <= N;
		invariant (forall k: int :: 0 <= k && k < i ==> res_perm[k] == old_perm[ new_perm[k] ]);
	{
		res_perm[i] := old_perm[ new_perm[i] ];
		i := i + 1;
	}
}

procedure swapElems(i: int, j: int) returns (local_perm: [int]int)
	requires 0 <= i && i < N;
	requires 0 <= j && j < N;
	modifies a;
	ensures (forall k: int :: k != i && k != j ==> a[k] == old(a)[k]);
	ensures a[i] == old(a[j]);
	ensures a[j] == old(a[i]);
	
	ensures perm_ok(local_perm);
    ensures is_perm(a, old(a), local_perm);
{
 	var tmp: int;
 	call local_perm := __new_perm__( );

	tmp :=    a[j];    a[j] :=    a[i];    a[i] := tmp;
	tmp := local_perm[j]; local_perm[j] := local_perm[i]; local_perm[i] := tmp;
}