@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 && i >=1 && i=< n
     	while (i =< n-1) {
	     i = i+1; 
	     s = s+(i*i);
        }
@end
--
Demo it as is, and then make the change from division to multiplication
in the invariant.