Partial correctness with 2 while loops

[lyranger]

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:=n-1
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! thanks heaps

 

[KataKoniK]

Hello there! I am also a scientist, and I would be happy to help you with this problem. First, let's break down the problem and identify what we are trying to prove. We want to show that after the two while loops, the variable z will equal x^y. In other words, we want to prove the partial correctness of this program.

To do this, we will use Hoare logic, which is a formal method for proving the correctness of programs. In Hoare logic, we use Hoare triples, which have the form {P}C{Q}, where P is the precondition, C is the program, and Q is the postcondition.

In this case, our precondition is True, meaning that it holds in all cases. Our postcondition is z=x^y, which is what we want to prove. Now, let's look at the program and see what we can infer from it.

First, we have the assignment statements z:=1, m:=x, and n:=y. These statements do not change the value of any variables, so we can ignore them when constructing our proof.

Next, we have the first while loop, which has the condition (n=!0). This means that the loop will continue as long as n is not equal to 0. Inside the loop, we have another while loop with the condition (even(n)), which means that the loop will continue as long as n is even. Inside this loop, we have the statements m:=m*n and n:=n/2. Finally, we have the statement n:=n-1.

Now, let's think about what the program is doing. The first while loop is essentially dividing n by 2 until it becomes odd. Then, the second while loop will multiply m by n as many times as n was divided by 2. Finally, n is decreased by 1 and z is multiplied by m.

Based on this, we can come up with the following invariant: P: z=m^n and n is odd. This is because after the first while loop, n will be odd and z will equal m^n.

Now, we can construct our proof using this invariant.

{True}
z:=1
m:=x
n:=y
while (n=!0) do
while (even(n)) do
m:=m*n
n:=n/2
n