LOOPS

First thing I am going to say is that I dislike analyzing a loop, or a recursion, especially proving them if they are correct or wrong. For example, the mergesort:

MergeSort(A,b,e):
if b == e: return
m = (b + e) / 2
MergeSort(A,b,m)
MergeSort(A,m+1,e)
# merge sorted A[b..m] and A[m+1..e] back into A[b..e]
for i = b,...,e: B[i] = A[i]
c = b
d = m+1
for i = b,...,e:
        if d > e or (c <= m and B[c] < B[d]):
                A[i] = B[c]
                c = c + 1
        else: # d <= e and (c > m or B[c] >= B[d])
                A[i] = B[d]
                d = d + 1

this is the example given in class.

first, we want to know the big theta of this loop, which is ok. Just unwinding it, using special case, (2^n, 3^n,...etc), and we will get the answer, no big deal.

Then we are to prove that T is non-decreasing, which is a little bit more annoying than the previous step. We have to show that it is bounded bewtween 2^(floor(n)) and 2^(ceiling(n)). Then we are pretty much done.

So that is it for the big theta, this is ok, some works

then we are going to the analyze the loop recursive binary search, this is what I dont like the most, maybe of all the course materials. so let's see the example in course

def recBinSearch(x, A, b, e) :
if b == e :
        if x <= A[b] :
                return b
        else :
                return e + 1
else :
        m = (b + e) // 2 # midpoint
        if x <= A[m] :
                return recBinSearch(x, A, b, m)
        else :
                return recBinSearch(x, A, m+1, e)

From CSC148, we know this is a correct recursive function,  but in CSC165, we only learned to prove if a loop is correct, so to prove a recursive function is brand new to me, but i figure it should be the same as to prove a loop. And no surprise, it is pretty much the same.... but this time, we were to arise with our own precodition, loop invariant, and the postcondition. Then we have to check if the input were comparable from input, for precondition, and check what the outcome should be for the postcondition, and then by having the precondition and the postcondition, we were to derive a loop invariant so that it will nicely bring us from preconditition to the postcondition...

This is not really hard to do, but there are extremely amount of work you have to do.
Especially the loop invariants, which sometimes are really hard to check them all at once, when there are many.

I know we have to learn this so that some day we can analyze others' codes, but it is just not my favourite thing.