Proving correctness of recursive list reversing algorithm.

Question

A list is either a value and a list, or NULL (empty list).

An example of a list would be [1, [2, [3, NULL]]] (could be read 1->2->3->NULL).

I recently needed a list reversing algorithm that was relatively fast, and I found the following:

list reverse(list first){
    if(first == null)
        return null

    if first.next == null
        return first

    list rest = reverse(l.next)

    first.next.next = first

    first.next = null

    return rest
}

Where .next is the reference to the next list, == is checking for equality and = is assignment.

This algorithm works, and it's explained here: https://stackoverflow.com/questions/14080758/reversing-a-linkedlist-recursively-in-c

However, I want to prove this always works. I've never proven the correctness of an algorithm, so I would like some help.

Answer 1

Intuitively it seems like a perfect application for proof-by-induction.

First prove that it works for null-length lists, which is pretty immediate just by inspecting the first few code lines.

Now assume that it reverses any list of arbitrary length up to $n$. Now introduce an abstract list of length $n+1$. For convenience ensure the list is constructed by appending an element to the head ("first").

By inspecting the relatively simple code, again, we see that the third statement down must reverse the $n$ tailing elements. This has to be true by assumption (see second paragraph above).

Now the remainder of the code seems to put the only outstanding element ("first") on the back of the list.

first.next

clearly still refers to the same element it did upon program start since "first" hasn't been modified yet even by the recursive call.

By induction, again, first.next is already at the end of the list. So now perhaps the line first.next.next = ... is well understood to put first at the end. And finally first.next = nul is needed to have a valid linked list.

The above is a proof-by-induction albeit with a lot of English and over explanation.

However, you should probably just run a few examples by such an algorithm and see that it works. If it ever fails, you'll find the error soon enough when you're debugging.

I am not certain whether your recursive algorithm is the most optimal. Also, check your language. Python for instance should have list-reversing.