@requires n >= 1

@ensures all(k, 0:n-2, a[k] =< a[k+1])

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

	i = n-1; 

        // must not declare k
        @invariant all(k, i:n-2, a[k] =< a[k+1]) && 
                   i>=0 && i=<n-1
	while (i > 0) {
	      j = 0;
	      @invariant all(k, 0:j, a[k] =< a[j]) &&
                         j>=0 && j=<i &&
			 all(k, i:n-2, a[k] =< a[k+1]) && 
                         i>=1 && i=<n-1 
              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
--