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
bal = readInt()
assert bal >= 0   # bal  is a global variable that holds an account's balance

# 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

5. In lecture, I pointed out that a global variable usually has its own global invariant. This is certainly true for a bank account. Please use your work from the previous question in this coding of a bank-account component:

#Q5.py:   a "bank account class":
bal = 0   # no money to start, but surely we will do some deposits  (-:
"""{ globalinv bal >= 0  }"""  # all methods must maintain this property

def withdraw(amt) :
    """{ pre  amt >= 0
         post bal + cash == bal_in
         return cash
    }"""
    global bal 
    if amt <= bal:
        bal = bal - amt
        cash = amt
    else :
        cash = 0
    # prove here that  bal >= 0 and bal + cash == bal_in
    return cash

def deposit(amt) :
    """{ pre amt >= 0
         post bal_in + amt == bal
    }"""
    global bal
    bal = bal + amt
    # The checker will prove this one for you *and* confirm the invariant!

# The checker will do this one, too:
def currentBalance() :
    """{ pre True
         post ans == bal
         return ans
    }"""
    ans = bal
    return ans