Week XII

For This week I would like to share my 'Problem Solving Episode' for the assignment 3 #1. Although the question was hard, but I really enjoyed the question after all. The question is :

def quotRem(n,m) :
#Precondition: n,m are natural numbers
# m is not 0
r = n
q = 0
while (not (m > r)) :
r = r - m
q = q + 1
# Postcondition: n = qm + r and 0 <= r < m

1) UNDERSTANDING THE PROBLEM
Since this function is not tested by machine, like Wing IDE, the only way to understand this problem is by reading line by line and understand what's is going on each line. However this would not be enough to understand perfectly, so I am going to prove this using loop invariant to see if the precondition implies the postcondition. In order to do that, we need to know the number of iteration(s) and when the loop terminates.
2) DEVISING A PLAN
Since we figure out that the number of iteration is n = q_i*m + r_i and it terminates E_i = r_i in N,
now, according to the standard tool for proof, we need to find which tool we are going to use it for the proof. In this case, PSI would be most effective and suitable.
3) CARRYING OUT THE PLAN
So this is the proof we get finally:
P(i) : If the loop has i iterations, then n = q_i*m + r_i and E_i = r_i in N,
if the prcondition is true. forall i in N, P(i)

Base case:
If i = 0, then r_i=n q_i=0. Since n = q_i*m + r_i = 0 * m + n = n,
this satisfies the postcondition, and also E_i = r_i = n in N by precondition,
so P(0) is true.

Induction Step:
Assume i in N and that P(i) is true. Assume there is an (i+1)th iteration of the loop and that precondition holds. By line 4, r_(i+1) = r_i - m and by line 5, q_(i+1) = q_i + 1. Then, n = q_(i+1) * m + r_(i+1) = q_i * m + m + r_i - m = q_i * m + r_i. Also, by P(i), r_i in N that r_i >= 0 and r_i >= m (by loop cond) So r_i - m = r_(i+1) >= 0 which is in N.
Therefore, precondition implies postcondition ( P(i) => P(i+1) )
4) LOOKING BACK
Overall, we found that this question is not that complicated but we have expected too high level.
Too much thinking sometimes lead us somewhere with nowhere to go. We actually have referred the lecture notes. There was not a similar question but the idea was quite similar. So the lecture note saved us. I am still wondering about if the loop invariant question always require PSI or not.
I want to see what kind of question requires PCI to prove.