// Notice the use of @assert just before break.  This is needed
// for the proof to go through.

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

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

	i = n-1;

        // must not declare k
        @invariant all(x=<y, i:n-1, a[x] =< a[y]) && 
                   i>=0 && i=<n-1
              
	while (i > 0) {
	      j = 0;
              swapped = false;
	      @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;
			 swapped = true;
                     }
                     j = j + 1;
              }
             if(not(swapped)) {
                @assert all(x=<y, 0:n-1, a[x]=<a[y])
	        break;
	     } else 
                i = i - 1;
       }
	
@end
--