function f( n : Z ) : Z
   	precondition n > 0
   	var x : Z
   	    y : Z
   	    u : Z
   	    v : Z
   	    r : Z
begin
	x:=1
	{n>0  /\ x=1}
	y:=1
	{n>0 /\ x=1 /\ y=1}
	r:=0
	{n>0 /\ x=1 /\ y=1 /\ r=0}
	while r<>n do
	invariant r =
	{ }
	begin
	    if r<n then
	    { n>0 /\ x>=1 /\ y>=1 /\ r >=0 /\ x mod 2 = 1 /\ y mod 2 =  /\ r > x-1)}
	    begin
	        r:=r+x
			{ }
	        x:=x+2
		end
	    else
	    begin
	        r:=r-y
			{ }
	        y:=y+2
		end
	end
	{ }
	{ }
	u:=(x-y) / 2
	{   }
	v:=((x+y)/ 2)-1
	{ }
	{ }
	f := n
end