function zad3( n : Z ) : Z
   	precondition n > 0
   	postcondition zad3 = n^2
   	var i : Z
   	    z : Z
            s : Z
            pi : Z
            ks : Z
begin
   	i := 1
   	{							}
   	z := 1
   	{ 							}
   	while i < n do
   	invariant 
   	begin
     		s := 1
		{ 						}
		pi := 2*i
		{ 	 					}
		ks := 1
		{ 						}
		while i+s<=n do
		invariant 
		begin
			z := z+pi+ks
			{ 					}
			i := i+s
			{ 					}
			ks := 4*ks
			{ 					}
			pi := 2*pi+ks
			{					}
			s := 2*s
		end
        end
   	{ 							}
   	zad3 := z
end