Well I just wrote the third test and completely imploded. I actually studied a fair bit however my brain just went completely blank on the first and second questions. The first one took me forever and I'm pretty sure I got it wrong as I ignored the typo until like half way through, tried changing it and just ended up getting really confused even though it wasn't actually that difficult. Then I did question 3 and by the time I got started on question 2 (which I'm fairly sure I could have answered correctly) I had so little time left that I just opted for the old "I cannot answer this question". Really disappointed with myself and wish I could just do it again. Oh well such is life, at least it will only be worth 6% with the amazing 236 marking scheme :)
This semester went by incredibly quickly and it still hasn't fully hit me that exams are next week. I'm really worried for every single class but cannot devote much time to either csc207 or csc236 since I have linear algebra (mat223) and stats (sta247) in the two days before. Honestly, I hated csc207 and stats (in my opinion two terribly designed courses), and feel that 236 was my favourite class. Unfortunately I was not able to devote as much time as I wanted to it and am still terrible with languages. Hopefully I will have enough time on Thursday to get a good grasp of the material and be able to get at least a semi decent mark on the exam.
Thanks for providing me with a somewhat enjoyable computer science course Danny, its been an interesting semester in csc236 at least. The course was quite refreshing when compared to my other courses and like csc165 last winter, it was my favourite course of the term. Hopefully I'll see you at some point next semester!
Friday, December 5, 2008
Tuesday, December 2, 2008
Problem Solving Session
A3 Q1
http://www.cdf.toronto.edu/~heap/236/f08/A3/a3.pdf
1. UNDERSTANDING THE PROBLEM
Since we have to prove program correctness, the first thing we have to develop is a loop invariant. Afterwards we have to show that the loop invariant holds true for the loop. Then we must prove partial correctness and then show termination.
2. DEVISING A PLAN
This problem is fairly similar to the multiplication program example in the textbook, so we will try to model our solution based on that somewhat. So we take a look at the program's loop and think about possible conditions that remain true before and after the loop. We know the pre and postconditions, so it is likely that invariant will contain at least some element of them.
3. CARRY OUT THE PLAN
The first thing we must do is find the loop invariant. The only one I could come up with is:
P(i): If the loop is executed at least i times then n = q_i*m + r_i.
I considered some other possibilities, such as negating the loop exit condition, however did not see a way to use this further in the proof.
We must prove this is the loop invariant:
Basis: Let i = 0.
Then q_0 = 0 and r_0 = n.
Then q_0*m + r_i = 0 + r_i = n
Then P(i)
Induction: Let j \in \N and assume that P(j) holds.
If m > r_j+1 then the loop doesn't execute and P(j+1) will be vaccuously true.
Otherwise r_j+1 = r_j - m and q_j+1 = q_j + 1.
Then r_j+1 + m*q_j+1 = (r_j - m) + (q_j + 1)
= r_j + m(-1 + q_j + 1)
= r_j + m*q_j
= n
Then P(j+1)
Thus P(i) \implies P(i+1) and P(i) is true by simple induction.
Now that we have the loop invariant, we must prove partial correctness and termination to show that the program is correct.
a) Partial Correctness:
Partial correctness is not very difficult to prove since we already proved our loop invariant. All that remains to be shown is the remaining part of the postcondition. We can model this solution on the Multiplication program's solution from Chapter 2 in the textbook.
P(i): Suppose the precondition holds. Then if quotRem(n,m) terminates, the
postcondition holds.
Assume the precondition holds and quotRem(n,m) terminates. Since it terminates,
the loop will be executed a finite number of times, lets call this natural
number 'k'. By the exit condition, m > r_k. m and r are natural numbers
by the precondition and m <= r_k-1 (must be true for the kth iteration of the loop to occur). Then r_k >= 0 since subtracting m from r_k-1 will never be less
than 0. Then 0 <= r_k < n =" q_k*m"> is decreasing.
Let k_i = r
Then k_i \in \N since r \in \N
Assume the loop is executed at least i+1 times.
Then k_i+1 = r - m
Then k_i+1 > k_i (since m cannot be 0 by the precondition)
Then the sequence is decreasing
Then P(i)
By the Principle of Well Ordering every set of decreasing natural numbers has a
smallest element. Then the sequence has a smallest element.
Therefore it is finite and the loop will terminate since an infinite set of
decreasing natural numbers is impossible.
We have now proven all elements necessary for this program's correctness and just need a concluding statement:
Then if quotRem(n,m) is called with arguments that satisfy the precondition,
it terminates, and when it does it satisfies the postcondition.
4. LOOKING BACK
Intuitively I can see that the program is correct and indeed carries out the division of numbers successfully. I am satisfied with my solution and have proved everything needed. There is no grey area that could allow for a loophole in the program's correctness. I don't think there are other ways to prove this program's correctness, unless you were able to come up with a unique loop invariant. The other parts of the proof are pretty mechanical and as such I feel confident that my answer is more than adequate.
http://www.cdf.toronto.edu/~heap/236/f08/A3/a3.pdf
1. UNDERSTANDING THE PROBLEM
Since we have to prove program correctness, the first thing we have to develop is a loop invariant. Afterwards we have to show that the loop invariant holds true for the loop. Then we must prove partial correctness and then show termination.
2. DEVISING A PLAN
This problem is fairly similar to the multiplication program example in the textbook, so we will try to model our solution based on that somewhat. So we take a look at the program's loop and think about possible conditions that remain true before and after the loop. We know the pre and postconditions, so it is likely that invariant will contain at least some element of them.
3. CARRY OUT THE PLAN
The first thing we must do is find the loop invariant. The only one I could come up with is:
P(i): If the loop is executed at least i times then n = q_i*m + r_i.
I considered some other possibilities, such as negating the loop exit condition, however did not see a way to use this further in the proof.
We must prove this is the loop invariant:
Basis: Let i = 0.
Then q_0 = 0 and r_0 = n.
Then q_0*m + r_i = 0 + r_i = n
Then P(i)
Induction: Let j \in \N and assume that P(j) holds.
If m > r_j+1 then the loop doesn't execute and P(j+1) will be vaccuously true.
Otherwise r_j+1 = r_j - m and q_j+1 = q_j + 1.
Then r_j+1 + m*q_j+1 = (r_j - m) + (q_j + 1)
= r_j + m(-1 + q_j + 1)
= r_j + m*q_j
= n
Then P(j+1)
Thus P(i) \implies P(i+1) and P(i) is true by simple induction.
Now that we have the loop invariant, we must prove partial correctness and termination to show that the program is correct.
a) Partial Correctness:
Partial correctness is not very difficult to prove since we already proved our loop invariant. All that remains to be shown is the remaining part of the postcondition. We can model this solution on the Multiplication program's solution from Chapter 2 in the textbook.
P(i): Suppose the precondition holds. Then if quotRem(n,m) terminates, the
postcondition holds.
Assume the precondition holds and quotRem(n,m) terminates. Since it terminates,
the loop will be executed a finite number of times, lets call this natural
number 'k'. By the exit condition, m > r_k. m and r are natural numbers
by the precondition and m <= r_k-1 (must be true for the kth iteration of the loop to occur). Then r_k >= 0 since subtracting m from r_k-1 will never be less
than 0. Then 0 <= r_k < n =" q_k*m"> is decreasing.
Let k_i = r
Then k_i \in \N since r \in \N
Assume the loop is executed at least i+1 times.
Then k_i+1 = r - m
Then k_i+1 > k_i (since m cannot be 0 by the precondition)
Then the sequence
Then P(i)
By the Principle of Well Ordering every set of decreasing natural numbers has a
smallest element. Then the sequence
Therefore it is finite and the loop will terminate since an infinite set of
decreasing natural numbers is impossible.
We have now proven all elements necessary for this program's correctness and just need a concluding statement:
Then if quotRem(n,m) is called with arguments that satisfy the precondition,
it terminates, and when it does it satisfies the postcondition.
4. LOOKING BACK
Intuitively I can see that the program is correct and indeed carries out the division of numbers successfully. I am satisfied with my solution and have proved everything needed. There is no grey area that could allow for a loophole in the program's correctness. I don't think there are other ways to prove this program's correctness, unless you were able to come up with a unique loop invariant. The other parts of the proof are pretty mechanical and as such I feel confident that my answer is more than adequate.
Subscribe to:
Comments (Atom)