verified selection sort

gistfile1.c

#include <vcc.h>

_(logic \bool sorted(int *buf, unsigned len) =
  \forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j])

_(typedef unsigned perm_t[unsigned];)

_(logic \bool is_permutation(perm_t perm, unsigned len) =
  (\forall unsigned i, j;
    i < j && j < len ==> perm[i] != perm[j]))

_(logic \bool is_permuted(\state s, int *buf, unsigned len, 
                         perm_t perm) =
  \forall unsigned i; i < len ==> 
      perm[i] < len && \at(s, buf[ perm[i] ]) == buf[i])

_(logic perm_t swap(perm_t p, unsigned i, unsigned j) =
      \lambda unsigned k; k == i ? p[j] : k == j ? p[i] : p[k])

void selection_sort(int *buf, unsigned len _(out perm_t perm))
	_(writes \array_range(buf, len))
	_(ensures sorted(buf, len))
	_(ensures is_permutation(perm, len))
	_(ensures is_permuted(\old(\now()), buf, len, perm))
{
	_(ghost \state s0 = \now() )
	_(ghost perm = \lambda unsigned i; i) 

	unsigned i, j;
	for (i = 0; i < len; ++i)
		_(invariant sorted(buf, i))
		_(invariant is_permutation(perm, len))
		_(invariant is_permuted(s0, buf, len, perm))
		_(invariant \forall unsigned x, y; x < i && i <= y && y < len ==> buf[x] <= buf[y])
	{
		unsigned k = i;
		for (j = i + 1; j < len; ++j)
			_(invariant j > i)
			_(invariant i <= k)
			_(invariant k < len)
			_(invariant \forall unsigned x; i <= x && x < j ==> buf[k] <= buf[x])
		{
			if (buf[j] < buf[k])
				k = j;
		}
		{
			int tmp = buf[i];
			buf[i] = buf[k];
			buf[k] = tmp;
			_(ghost perm = swap(perm, i, k))
		}
	}
}