Exercises for Chapter 2

10 points. Due September 9, 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 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 9th, 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.

# Q1.py
x = readInt()
assert x > 0
x = x + 1
x = x + 1
# prove here:  x > 2

# Q2.py
x = readInt()
y = x + 2
z = y - 1
# prove here:  (y > x) and (z > x)

# Q3.py
x = readInt()
assert x > 0
y = 2 * x
# prove here:  y >= 2      (hint: prove first that  x >= 1)
print "x =", x, " y = , y

# Q4.py
x = readInt()
y = 2 * x
x = x + 1
y = y + 2
# prove: y == x * 2

5. Here is some code from the heart of a coinflip game, where a player starts with some money and then flips a coin to try to double it (or lose it):

# Q5.py
# import random                   # this imports a Python package named  random
# money = random.randrange(1,100) # this assigns a random number between 10 and 99
money = readInt()                 # the checker doesn't know about  random.randrange  )-:
assert money > 1  and  money < 100 # so we fake it...

# coinflip = random.randrange(0,2)   # assigns 0 or 1 to coinflip
coinflip = readInt()                 # and we fake it for now:
assert coinflip == 0  or  coinflip == 1

if coinflip == 1 :  # a winner!
    money = money * 2
else : # a loser
    money = 0

# Prove here that
#   (coinflip == 1 and  money > 0)  or  (coinflip == 0 and money == 0)

6. Here is software for a cash withdrawal that one might find within an ATM:

# Q6.py
balance = readInt()    # get this info from the bank's database
assert balance >= 0
startbal = balance

deduction = readInt()  # get this info from the customer

if deduction > balance :  # did the customer ask for too much cash ?
    cash = 0
else :
    cash = deduction
    balance = balance - cash

# prove here this correctness property:
#      balance >= 0  and  cash + balance == startbal

print "you have withdrawn", cash, "dollars from your account."