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 AI answers yet. The ability to request AI answers is coming soon!
There are no human answers yet. A form for humans to post answers is coming very soon!