Skip to content

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.

  1. Find a loop invariant I (that can help you prove this program)
  2. Find the wp for the loop (using I and Q)
  3. 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
Show that 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.