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

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

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

来源

2013-03-12 Yeesum Chan

可能有帮助：http://stackoverflow.com/questions/7699692/proof-by-induction-of-pseudo-code – jbabey 2013-03-12 12:25:34

首先您必须具体说明您的意思是正确性（即您要检查代码的规范;另请参阅https://stackoverflow.com/a/16630693/476803）。让我们假设正确性这里指

的permute每个输出给定的字符串的置换。

然后，我们可以选择执行归纳的自然数。对于递归函数permute，我们可以选择low或high或其某种组合。

当读取实现时，显然输出字符串的某些前缀的元素不会更改。此外，这个前缀的长度在递归期间增加，因此其余的后缀（其长度为high - low）减小。因此，让我们在high - low上进行归纳（假设low <= high，这是合理的，因为我们最初使用0表示低，一些字符串的长度为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),生成的输出中low（最高为high）之后的任何字符，我们生成了low和high之间的字符排列。这一步（我在这里省略了，因为我只是想证明你原则上可以如何使用归纳）就是证明。

最后，通过对0和low实例str.length上述事实为high我们有一个非递归permute的每一个输出的str置换。

注意：以上证明只显示每个输出是一个置换。然而，知道所有排列都被打印出来也可能是有趣的。

来源

2013-07-29 06:02:04 chris

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

回答

相关问题