1

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}
  • I can see how this -could- relate to testing. Definitely. Proving the correctness of an algorithm is the nuclear option of quality assurance, and for anything but trivial programs is practically impossible. However, this particular question isn't really a question. Rather, it's an assignment. We solve problems, yes, but we don't just do assignments. What are you missing in terms of understanding this problem? – corsiKa Apr 22 '16 at 13:46

Browse other questions tagged or ask your own question.