I am trying to prove the correctness of a simple recursive program, its the function where it returns a string but reversed.

Code:

def rev(s):
if len(s)<2
return s
return s[-1]+rev(s[:-1])

This is what i have for the proof, I am stuck in the induction step. What am I doing wrong?

P(k): If s is a string and k is len(s), then rev(s) terminates and returns a reverse string of s.

Prove for all k in N, P(k). [PSI]

Basis: For k=0

Then rev(“”) returns “”. [line 1,2]

Therefore reverse of “” is “”, as wanted.

For k=1

Let c be a string s.t. len(c)=k

Then rev(c) returns c. [line 1,2]

Therefore reverse of c is c, as wanted.

I.S.: Let k be in N s.t. k>=1 (@)

Suppose P(k) [I.H.]

Let d be a string s.t. |d|=k+1 i.e. |d|>=2 since k+1>=2 [(@)] (*)

d[-1]+rev(d[:-1]) = rev(d[-1])+rev(d[:-1])

= rev(d[-1]+d[:-1])

= rev(d) [I.H.]

Therefore P(k+1) holds.