@requires n >= 1

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

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

	i = n-1; 

        @invariant all(x=<y, i:n-1, a[x] =< a[y]) && 
                   i>=0 && i=<n-1
	while (i > 0) {
	      j = 0;
	      @invariant all(k, 0:j, a[k] =< a[j]) &&
                         j>=0 && j=<i &&
			 all(x=<y, i:n-1, a[x] =< a[y]) && 
                         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
--