how to prove the correctness of recursive algorithm?

Question

private static void swap(char[] str, int i, int j){
  char tmp = str[i];
  str[i] = str[j];
  str[j] = tmp;
}

public static void permute(String str){
  permute(str.toCharArray(), 0, str.length());
}

private static void permute(char[] str, int low, int high){
  if(low == high){
    System.out.println(str);
  } else {
    for(int i = low; i < high; i++){
      swap(str, low, i);
      permute(str, low+1, high);
      swap(str, low, i);
    }
  }
}

I implemented a recursive method for string permutation. But I got a question: How to prove the correctness of this code by using induction? I really got no idea.

Answer 1

First you have to say concretely what you mean by correctness (i.e., the specification against which you want to check your code; see also https://stackoverflow.com/a/16630693/476803 ). Lets assume that correctness here means

Every output of permute is a permutation of the given string.

Then we have a choice on which natural number to perform induction. For the recursive function permute, we have the choice between either of low or high, or some combination thereof.

When reading the implementation it becomes apparent that there is some prefix of the output string whose elements do not change. Furthermore, the length of this prefix increases during the recursion and thus the remaining suffix, whose length is high - low, decreases. So lets do induction on high - low (under the assumption that low <= high, which is sensible since initially we use 0 for low and the length of some string for high, and the recursion stops as soon as low == high). That is, we show

Fact: Every output of permute(str, low, high) is a permutation of the last high - low chars of str.

• Base Case: Assume high - low = 0. Then the statement is vacuously true since it has to hold for the last 0 characters (i.e., for none).

• Step Case: Assume that high - low = n + 1. Furthermore, as induction hypothesis (IH) we may assume that the statement is true for n. From high - low = n + 1 we have that high - (low + 1) = n (since high must be strictly larger than low for high - low = n + 1 to hold). Thus, by IH, every output of permute(str, low+1, high) is a permutation of the last high - (low + 1) characters of str.

  Now comes the point where we actually have to prove something. Namely that by swapping, in an output generated by permute(str, low+1, high), the low-th character of str with any character after low (up to high), we generate a permutation of characters between low and high. This step (which I omit here, since I just wanted to demonstrate how you could in principle use induction) concludes the proof.

Finally, by instantiating the above Fact with 0 for low and str.length for high we have that every output of the non-recursive permute is a permutation of str.

Note: The above proof only shows that every output is a permutation. However, it might also be interesting to know that in fact all permutations are printed.