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

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

4

1 回答 1

0

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

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

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

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

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

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

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

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

最后，通过用for和for实例化上述Fact ，我们得到非递归的每个输出都是 的排列。0lowstr.lengthhighpermutestr

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

于 2013-07-29T06:02:04.783 回答