How to prove partial correctness? [closed]

Question

Consider the following pseudo-code:

begin 
x:= 0; 
y:= 1; 
z:= 1; 
while y <= n do 
x:= x+1; 
z:= z+2; 
y:= y+z; 
od 
sqrt := x; 
end 

How would I prove the partial correctness of the above code with respect to the following predicates:

Pre: {n>=0} 

Post: {sqrt2 <= n and n < (sqrt+1)2 
) 

That is,

{Pre} 
begin 
x:= 0; 
y:= 1; 
z:= 1; 
while y <= n do 
x:= x+1; 
z:= z+2; 
y:= y+z; 
od 
sqrt := x; 
end 
{Post}