In-class Assignment 3 (updated)
In class assignment 3 (due Thursday 10:59 AM, right before class).
Program 1
{x <= 10} #P
while x != 10:
x := x + 1
{x == 10} #Q
Prove that the above program is corret with respect to the given pre and post conditions P
and Q
.
- Find a loop invariant
I
(that can help you prove this program) - Find the
wp
for the loop (usingI
andQ
) - Prove the program is correct (by showing the verification condition
P => wp(S, Q)
is true)
Program 2
def do_something_2(A):
assert A >= 0 # P
x = 1
y = A
z = 1
while True:
# loop invariant I: 2**A == (x+z) * 2**(y-1)
if not (y != 0 or z != x):
break
if z == 0:
y = y - 1
z = x
else:
x = x + 1
z = z - 1
assert x == 2 ** A # Q
do_something_2
is correct wrt to the given specifications P
and Q
using the provided loop invariant I
. More specifically, do the following (see example for do_something_1
in class notes, you do not need to follow this exact order)
1. Show I
holds when the loop is entered the first time
2. Show when loop exits, I
and the negation of the loop guard implies Q
3. Show that assuming I
holds at the loop entrance, I
will also hold after the loop body is executed.