如何證明遞歸算法的正確性？

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

如何證明遞歸算法的正確性？

回答

相關問題