Exercises for Chapters 2 and 3

10 points. Due February 3, 10pm

For each of the problems that follow, please check your work with the CIS301 proof checker, using the checker's v (verbose) option. When you submit your work, please make a folder and place in it the file of your original proof (a py file) and the html file generated from it by the checker. Then, zip the folder and submit the zipped folder to the CIS301 page at K-State online.

Bring your work with you to class on the 3rd, so that we can review it on the board.

Please do your own work --- whatever you submit must be stored in your brain as well as in your computer files.

1. Prove this program is correct:

# Q1.py
x = readInt()
y = readInt()
if y > x :
    ans = y - x
else :
    ans = x - y

# prove  ans >= 0

2. This program cannot be proved correct --- there is an error in its coding. Change one line only in the program and prove the final correctness property:

x = readInt()
if x > 0 :
    y = x + 1
else :
    y = 0 - x
# prove here that  y > 0  and  y > x

3. The checker is programmed to verify automatically simple pre-post-conditions for simple functions. For the example program below, the checker will automatically verify sub. Now, you must write the proof that calls sub to obtain a final correctness property:

# Q3.py
# The checker verifies automatically that  sub  satisfies its pre-post-conditions:
def sub(x, y) :
    """{ pre  x > y
         post z < 0 and z + x == y
         return z
    }"""
    z = y - x
    # The checker automatically proves   z < 0 and z + x == y.
    return z

# Your work starts here:
a = readInt()
assert a > 0
b = sub(2 * a, a)
# Prove here that   a == 0 - b

4. Somethimes functions must change the value of a global variable, x. The update is stated in the function's postcondition in terms of x's new value and its orginal value, x_in.

Here is a component for cash withdrawal from an ATM that updates global variable bal; prove the function is correct.

# Q4.py
assert bal >= 0   # bal  is a global variable that holds an account's balance
# the checker will warn that "bal isn't declared", but it's ok for now....

# function  withdraw  extracts  amt  from the balance and returns  cash
def withdraw(amt) :
    """{ pre  bal >= 0 and amt >= 0
         post bal >= 0 and bal + cash == bal_in
         return cash
    }"""
    global bal  # Python requires this line when a function changes a global var
    # bal_in = bal  (The checker adds this "ghost assignment")
    # This generates a new premise you can use:  bal == bal_in
    if amt <= bal:
        bal = bal - amt
        cash = amt
    else :
        cash = 0
    # Prove the postcondition here; the checker can't do this one alone.
    return cash