Exercises for Chapters 2 and 3

As in the other examples and exercises, I have used blank spaces to indent the code lines. Please be careful not to mix tabs and blanks in your indentations!

Bring your work with you to class on the 7th, 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.

A USEFUL STRATEGY: For each of these questions, paste the program text into a file, Qn.py, and run the checker on it, verbose mode, as is. The checker will generate a load of internal information flow that you can use as a start for writing the internal proofs.

1. Prove this program is correct:

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

# GOAL: prove  ans > 0

2. This program cannot be proved correct --- there is an error in its coding. (You can find the error by asking the checker to analyze the program without any proof steps. Then read it, then insert a partial proof and see where the checker complains.) Change or add one line only in the program and prove the correctness property:

# Q2.py
x = readInt()
if x > 0 :
    y = x
    x = x - 1
else :
    y = 0 - x

# GOAL: prove here that  y > 0  and  y > x

3. Prove me:

# Q3.py
x = readInt()
if x < 0 :
    x = 0 - x
else :
    if x > 0 :
         pass
    else :
         x = x + 1

# GOAL: prove here that  x > 0

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

# Q4.py
# The checker verifies automatically that  sub  satisfies its pre-post-conditions:
def withdraw(money, amt) :
    """withdraws  amt  from account  money  and returns the new balance of  money"""
    """{ pre  money >= amt
         post balance == money - amt
         return balance
    }"""
    balance = money - amt
    return balance

# Code inside an ATM controller:
accountbalance = 100
# ask user how much cash they want from the ATM:
cash = readInt("Type an amount to withdraw from your account:")
assert cash <= 80
newbalance = withdraw(accountbalance, cash)
accountbalance = newbalance
# GOAL: Prove here that   accountbalance >= 0

5. When a function changes the value of a global variable, g, the function's postcondition might be stated in terms of g's new value and its value on function entry, named, g_in.

Here is another method for cash withdrawal from an ATM. It maintains a global variable bal; prove the function is correct.

# Q5.py
bal = 100  # bal  is a global variable that holds an account's balance
"""{ 1.  bal >= 0    premise   }"""  

# function  withdraw  subtracts  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 will add this "ghost assignment" ---
    #                 look at its output in "verbose mode".)
    # You can use this premise:  bal_in == bal
    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

6. A global variable usually has its own global invariant. This is true for a bank account. Paste your work from the previous question into this coding of a bank-account component:

#Q6.py   
# class BankAccount {      # a "bank account class"
bal = 0                         # field that holds the account's balance
"""{ globalinv bal >= 0  }"""   # all methods must maintain this property
                                #   This is the *class invariant*
def withdraw(amt) :
    """removes  amt  from  bal,  provided precondition holds, and returns amount removed."""
    """{ 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) :
    """adds  amt  to  bal."""
    """{ 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() :
    """returns value of  bal."""
    """{ pre True
         post ans == bal
         return ans
    }"""
    ans = bal
    return ans

# }   # end class BankAccount