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

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://stackoverflow.com/a/16630693/476803(。让我们假设正确性在这里意味着

CCD_ 1的每个输出都是给定字符串的一个置换。

然后我们可以选择对哪个自然数进行归纳。对于递归函数permute，我们可以在low或high或它们的某种组合之间进行选择。

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

事实：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的置换。

注意：以上证明仅表明每个输出都是置换。然而，也可能有意思的是，事实上所有排列都是打印出来的。