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

@requires n >= 1
@ensures all(k, 0:n-2, a[k] =< a[k+1])
@program 
	@var i, j, n, temp: int
        @var flag : bool
	@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]) && i>=1 && i=<n-1 &&
			 all(k, i:n-2, a[k] =< a[k+1]) && j>=0 && j=<i
              while (j < i) {
                     if (a[j] > a[j+1]) {
                         temp = a[j];
		         a[j] = a[j+1];
		         a[j+1] = temp;
			 flag = true;
                     }
                     j = j + 1;
              }
             if(not(flag)) {
                @assert all(k, 0:i-1, a[k] =< a[k+1])
	        break;
	     } else 
                   i = i - 1;
             flag = false;
       }
	
@end
--