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