Exercises for Chapter 4

Please check your answers to Questions 1-3 with the CIS301 proof checker; use the verbose (v) option. Please type your answer to Question 4 as a text file. Place all answers in a zipped folder and submit at K-State Online. We will review several of these questions at classtime on October 18, so please bring a copy of your work to class.

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

1. Insert the correctness proof for this loop program:

n = readInt()
x = 0
y = n
while y != 0 :
    """{ invariant ???
         modifies  y, x  }"""
    y = y - 1
    x = x + 1

# PROVE HERE THAT:  x == n
print y

2. Prove that the function satisfies its postcondition.

def multiply(a,b):
   """{ pre  a >= 0
        post ans == a * b
        return ans
   }"""
   ans = 0
   i = a
   while i != 0:
       """{ invariant ???
            modifies  i, ans
       }"""
       ans = ans + b
       i = i - 1
   return ans

3. Here is a program that computes the remainder ("modulo") from dividing q by d (that is, q % d). The code is stated as how it was once wired in primitive CPUs. Fill in the missing loop test and assignment. Then, complete the correctness proof:

q = readInt()
d = readInt()
assert q >= 0
assert d >= 0
n = 0
rem = q
"""{ 1. q >= 0     premise
     2. d >= 0     premise
     3. n == 0     premise
     4. rem == q   premise
     5. rem >= 0   subst 4 1
     6. (d * n) + rem == q  algebra 3 4
     7. return 6 5          # USE THESE TO ENTER LOOP
}"""
while ??? :
    """{ invariant  (d * n) + rem == q  and  rem >= 0
         modifies  rem, n   }"""
    rem = ???
    n = n + 1

# LOOP ENDS
"""{
     # prove here: (d * n) + rem == q  and (0 <= rem  and  rem < d)
}"""

4. Here is a function:

def double(n) :
    ans = 0
    i = 0
    while i != n :
        ans = ans + 2
        i = i + 1
    return ans

For all legal input integers, n, from the set, {0,1,2,3,...}, double(n) returns an answer that equals 2*n