如何证明递归算法的正确性？

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);
    }
  }
}

我实现了一种用于字符串排列的递归方法。但是我有一个问题：如何用归纳法证明这段代码的正确性？我真的不知道。

Answer 1

首先，您必须具体说明 正确性 的含义（即，您要检查代码的规范；另请参阅 https://*.com/a/16630693/476803 ）。让我们假设这里的 正确性 意味着

permute 的每个输出都是给定字符串的排列。

然后我们可以选择对哪个自然数进行归纳。对于递归函数permute，我们可以选择low 或high，或两者的组合。

在阅读实现时，很明显输出字符串的某些前缀的元素不会改变。此外，该前缀的长度在递归期间增加，因此长度为high - low 的剩余后缀减少。因此，让我们对high - low 进行归纳（假设low <= high，这是合理的，因为最初我们使用0 表示low，某些字符串的长度用于high，并且递归在low == high 时立即停止）。也就是说，我们展示了

事实：permute(str, low, high) 的每个输出都是str 的最后一个high - low 字符的排列。

• 基本情况：假设high - low = 0。那么该语句是空洞的，因为它必须保留最后一个 0 字符（即，没有）。

• 步骤案例：假设high - low = n + 1。此外，作为归纳假设 (IH)，我们可以假设该陈述对于n 是正确的。从high - low = n + 1 我们得到high - (low + 1) = n（因为high 必须严格大于low 才能保持high - low = n + 1）。因此，根据 IH，permute(str, low+1, high) 的每个输出都是 str 的最后一个 high - (low + 1) 字符的排列。

  现在到了我们实际上必须证明某些事情的时候了。也就是说，通过在permute(str, low+1, high)生成的输出中，str的第low个字符与low之后的任何字符（最多high）交换，我们生成low之间的字符排列和high。这一步（我在此省略，因为我只是想说明原则上如何使用归纳法）结束了证明。

最后，通过用0 为low 和str.length 为high 实例化上述Fact，我们得到非递归permute 的每个输出都是一个排列str.

注意： 上面的证明只表明每个输出是一个排列。但是，知道实际上 所有 排列都已打印出来可能也很有趣。