Partial correctness with 2 while loops

  • Thread starter lyranger
  • Start date
  • #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:=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!! thx heaps
 

Attachments

Answers and Replies

Related Threads on Partial correctness with 2 while loops

  • Last Post
Replies
5
Views
5K
  • Last Post
Replies
2
Views
644
  • Last Post
Replies
1
Views
2K
  • Last Post
Replies
2
Views
2K
  • Last Post
Replies
7
Views
1K
  • Last Post
Replies
15
Views
5K
  • Last Post
Replies
1
Views
2K
Replies
5
Views
4K
Replies
4
Views
855
Replies
1
Views
1K
Top