 #1
 9
 0
1. Homework Statement [/b
Here is a question on proof of partial correctness with 2 while loops
with Hoare logic
{True}
z:=1
m:=x
n:=y
while (n=!0) do
while (even(n)) do
m:=m*n
n:=n/2
n:=n1
z:=z*m
{z=x^y}
I do know how to solve it when there is only 1 loop: finding invariant P and follow the usual steps.
But I have no idea how to tackle this one. Any help would be appreciated!! thx heaps
Here is a question on proof of partial correctness with 2 while loops
with Hoare logic
{True}
z:=1
m:=x
n:=y
while (n=!0) do
while (even(n)) do
m:=m*n
n:=n/2
n:=n1
z:=z*m
{z=x^y}
Homework Equations
The Attempt at a Solution
I do know how to solve it when there is only 1 loop: finding invariant P and follow the usual steps.
But I have no idea how to tackle this one. Any help would be appreciated!! thx heaps
Attachments

6.7 KB Views: 331