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
(Hint: the checker program sometimes has trouble proving assertions
with polynomials (multiplications), since this exceeds the
checker's automated expertise in linear arithmetic.
If algebra fails to prove a line, try subst instead.)
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
In place of testing the function, use a
mathematical induction argument to prove this claim: