// Appears to work but does not.

@requires n >= 1

@ensures all(p=<q, 0:n-1, a[p]=<a[q])

@program 
	@var i, j, n, temp : int
	@var a : int[]

	i = n-1; 

        @invariant all(p=<q, i:n-1, a[p]=<a[q]) &&
                   all(p<i+1=q, 0:n-1, a[p]=<a[q]) &&
                   i>=0 && i<n
	while (i > 0) {
	      j = 0;
	      @invariant 
			all(p<i+1=q, 0:n-1, a[p]=<a[q]) &&
			all(p=<q, i:n-1, a[p]=<a[q]) &&
                        all(k, 0:j, a[k]=<a[j]) &&
                        0=<j && j=<i && i<n && i > 0
              while (j < i) {
                     if (a[j] > a[j+1]) {
                         temp = a[j];
		         a[j] = a[j+1];
		         a[j+1] = temp;
                     }
                     j = j + 1;
             }
             i = i - 1;
	}
@end
--