function sum( n :Z) : Z
	precondition n_ge_one : n >=1
	postcondition sum=n*(n+1)/2
	var x : Z
		y : Z
begin
	{ x = x /\ n >= 1 }
	x := 1
	{ x = 1 /\ n >= 1 }
	{ y = y /\ x = 1 /\ n>=1 }
	y := 0
	{ y = 0 /\ x = 1 /\ n>=1 }
	while x <= n do
	invariant y = (x-1)*x/2 /\ n>=1 /\ x <= n + 1
	begin
		{ y + x = (x-1)*x/2 + x /\ n>=1 /\ x < n + 1 }
  		y := y + x
  		{ y = (x-1)*x/2 + x /\ n>=1 }
  		{ y = (x + 1 - 2)*(x + 1 - 1)/2 + x + 1 - 1 /\ n>=1 /\ x < n + 1}
  		x := x + 1
  		{ y = (x-2)*(x-1)/2 + x-1 /\ n>=1 /\ x <= n + 1}
  	end
  	{ y = n*(n+1)/2}
  	sum := y
  	{ sum = n*(n+1)/2}
end