Problem set 4

Problem set 4 was OK, i missed a perfect score because I did not use the induction hypothesis but here is my solution: (Please note that blogspot does not like spaces so indentation is a problem; sorry about that)

def revString(s):
if len(s) <>
else: return revString(s[1:]+s[0])

(1) Define our P(n)
{
____P(n) = /forall s /in Strings+ { if len(s) == 1: revString(s)
____else if len(s) > 1: revString(s[1:]+s[0])
}

Lets assume that the program does not take empty strings (strings with length 0) and lets denot all strings with positive lengths but Strings+. i.e: /forall x /in Strings+, len(x) > 0.

Proof:
Base case:
len(s) = 1

Assume s /in Strings+
{

__Then s is a string with at least 1 element
__Then len(s) = 1 and 'if' condition is satisfied
__Then revString() executes line: 'if len(s) is less than 2: return s
__Then revString() is correct.

}
Then /forall s /in Strings+, len(s) < 2 =""> revString() is correct and our base case passes=> Post condition is true.

Inductive case:

Assume n /in N #Generic natural number
_Assume s /in Strings+
__Assume i=0_V^n P(i) (*) (Want to prove P(n+1))
___Assume len(s) >= 2

{
____Then 'if' condition is false and line 'if len(s) <>
____Then line 'else: return revString(s[1:] + s[0])' is executed.
____Then len(s[0])=1 && (len(s[0]) <= len(s[1:]).
____Since len(s[0]) = 1, from our base case we know that len(s) == 1 ==> return s.
____So return revString(s[1:]) + s[0] # *1 = s[0] part is then true.
____Then revString(s[1:]) is called.

____Case 1: len(s[1:]) == 1:
_____by base case, if len(s) == 1: then return s
_____Then s[1:] is returned and revString() is correct.
_____s[1:] + s[0] means string returned is reversed ==> Post condition is true.

____Case 2: len(s[1:]) >= 2:
_____Then line 'else: return revString(s[1:] + s[0])' is called.
_____# s[0] by *1 is true
_____Then by (*), revString() is correct.
_____==> Post condition is true
}

___Then revString() is correct # proof by cases
__Then P(n+1)
_Then i=0_V^n P(i) => P(n+1) # intro =>
Then /forall s /in Strings+, i=0_V^n P(i) => P(n+1) #intro
/forallThen /forall n /in N, /forall s /in Strings+, i=0_V^n P(i) => P(n+1) #intro /forall

Then Post condition holds and revString() is correct