Problem-Solving Episode

Since I feel most uncomfortable with proving the recursive, so I was looking for some kind of proof related to recursive function . Luckily, though I was in the morning section but I know someone in the evening section who is able to borrow his second term test to me. I found a interesting one:

def CheckPal(s):
1 #Precondition: s is a python string.
2 if len(s) <>
3 else:
4 s_inner = s[1:len(s) - 1]
5 return s[0] == s[len(s)-1] and CheckPal(inner)
6 # Post return true if s is a palindrome.

1. Understanding the problem
As the function is never tested on a machine, we can read through it and find it might work, but that would not be sufficient to justify this function behaves exactly what we expect. The function is known, and to prove it is correct is what we are heading for.

2.Devising a plan
According to standard proof "pattern" we have been using in this course, it will be either a simple or complete induction. Where in this case, strong induction seems more suitable.

3.Carrying out the plan
So I argue P(n): if n = len(s), the precondition implies the post condition, I claim that \forall n \in N, P(n) always holds for true.

Here is the proof:
Assume n \in N, and assume P(0) and P(1) and ...... and P(n-1) is true, assume pre condition holds for any arbitrary string s.

Case 1: Assume s is a python string and n palindrome and a character itself is a palindrome too, which in both cases satisfying the post condition. Therefore P(0) and P(1) is true.

Following cases are all based on s is a python string, which satisfies the pre condition.

Case 2A: If n >= 2 and n is even, line 1 fails and line 4 gets executed. A sub string is taken from the second letter to the second last character. As such, the length of the newly created string would be a even number as well. After that, line 5 runs and it will evaluate s[0] == s[len(s) - 1], which is checking if the first and last character is the same, and this is exactly what we are heading for. Meanwhile, this line also generated a recursive call to evaluate the s_inner string to see if it is palindrome, the recursive call will follow the steps below, moving towards the post condition, therefore P(n)

Case 2B: If n >= 2 and n is odd, line 1 fails too, a substring is formed from the second character to the second last character and set this string to variable s_inner. However the length of this string is odd. Line 5 will evaluate s[0] == s[len(s) - 1] as well as CheckPal(s_inner). Differ from case 2A, this recursive call will sooner or later left with a string containing only one character, which is saying n = 1, at that time line 2 will executes, and if it is palindrome, the call stack will return true all the way to the main function call, otherwise it will return false, which in both cases satisfying the post condition.

So P(n).

4. Looking Back
This loop is not a very complicated one, and for some reason I do believe I can prove it with the simple induction, but the even or odd length will be tricky if I am with the simple induction. Proving the program's correctness is essential not only theoretically, but also in practice, if a function does not behaves what we like it to be, and we can have a pretty good idea of where it can be wrong if we were to prove it.