@requires n >= 1
@ensures s = n*(n+1)/2
@program 
	@var i, n, s : int
     	s = 1;  
     	i = 1;  
        @invariant s == i*(i+1)/2 && i=<n
     	while (i < n) {
	     i = i+1; 
	     s = s+i;
          }
@end
--