@function sigma : int -> int

@axiom A1:  sigma(1) = 1
@axiom A2:  all n:int. n > 1 ==> sigma(n) = n*n + sigma(n-1)

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