@requires n >= 1

@ensures all(k, 0:n-1, max >= a[k]) 
	 	&&
	 exists(k, 0:n-1, max = a[k])

@program 
	@var i, max, n : int
        @var a : int[]

	max = a[0];
        i = 1;
        @invariant all(k, 0:i-1, max >= a[k]) &&
	           exists(k, 0:i-1, max = a[k]) &&
		   i >= 1 && i =< n
        while (i < n) {
		if (max < a[i])
		    max = a[i];
		i = i + 1;
	   }

@end
--
Meaning of all(k, low:high, property):

(forall k)[low <= k <= high  ==> property] 

Meaning of exists(k, low:high, property):

(exists k)[(low <= k <= high) && property]