Asked by Jack
Consider the following program (written in 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
Prove the partial correctness of the program 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}
begin
x:= 0;
y:= 1;
z:= 1;
while y <= n do
x:= x+1;
z:= z+2;
y:= y+z;
od
sqrt := x;
end
Prove the partial correctness of the program 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}
Answers
There are no human answers yet.
There are no AI answers yet. The ability to request AI answers is coming soon!
Submit Your Answer
We prioritize human answers over AI answers.
If you are human, and you can answer this question, please submit your answer.