點此開啟題目頁面

先給出AC程式碼, 然後給出程式正確性的形式化證明.

//CH0303_遞迴實現排列型列舉
#include <iostream>
#include <cstdio>
#include <vector>
using namespace std;
const int MAX = 1e2;
int n;
vector<int> choosn;
bool used[MAX];//used[i]為true對應choosn中包含元素i, false則不包含 
void solve(){
	if(choosn.size() == n){
		for(int i = 0; i < n; ++i) cout << choosn[i] << " "; cout << endl;
		return;
	}
	for(int i = 1; i <= n; ++i)
		if(!used[i]) 
			used[i] = true, choosn.push_back(i), solve(), choosn.pop_back(), used[i] = false;
} 
int main(){
	scanf("%d", &n);
	solve();
	return 0;
} 
 

程式正確性的形式化證明:

    定義集合 = { x | x為一次對solve的呼叫, 且choosn.size() = i, choosn[0...i - 1]對應{1...n}取i個元素的一個排列, 且對於所有的j  choosn[0...i - 1], 滿足used[ j ]為false, 除此之外used中的元素均為true }

    歸納基礎: 對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態.

    遞推: 假設對於集 (2 =< k <= n)中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前choosn.size()個元素為choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 容易推知設對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態.

    綜上述, 對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 進一步分析, 對於(初始choosn為空)中的所有元素能夠按字典序遞增的順序列印1,...,n的所有全排列. 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 從而程式正確性得證. 

    常見的用於生成全排列的還有如下演算法, 但是下面這種演算法並非按照字典序遞增(或遞減)列印每個全排列, 同上, 在給出程式碼後將給出程式正確性的形式化證明. 

//CH0303_遞迴實現排列型列舉
#include <iostream>
#include <cstdio>
using namespace std;
const int MAX = 1e2;
int seq[MAX], n;
void solve(int cur){
	if(cur == n){
		for(int i = 1; i <= n; ++i) cout << seq[i] << " "; cout << endl;
		return;
	}
	for(int i = cur; i <= n; ++i)
		swap(seq[cur], seq[i]), solve(cur + 1), swap(seq[cur], seq[i]);
}
int main(){
	scanf("%d", &n); for(int i = 1; i <= n; ++i) seq[i] = i;
	solve(1);
	return 0;
} 

 定義集合 = { x | x為一次對solve(i)的呼叫, 且seq[1...n]對應1...n的一個全排列}

     歸納基礎: 對於集中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前n - 1個元素對應seq[1...n - 1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態.

    遞推. 假設對於集 (3 =< k <= n)中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前k - 1個元素對應seq[1...k - 1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 對於集中的元素, 根據程式第12, 13行的程式碼很容易確定程式均能夠按字典序遞增的順序列印1,...,n的所有前k - 2個元素對應seq[1...k - 2]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態.

    綜上述, 對於集中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前1個元素對應seq[1...1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 再次根據根據程式第12, 13行的程式碼可知對於集中的所有元素, 程式均能夠按字典序遞增的順序列印1,...,n的所有全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 也即程式正確性得證.

    特別的, 如果將上述程式修改為下面所示程式碼, 那麼仍能夠按照字典序遞增輸出1...n的所有全排列, 並且AC, 至於程式正確性的證明過程, 此處不再贅述.

//CH0303_遞迴實現排列型列舉
#include <iostream>
#include <cstdio>
#include <map>
using namespace std;
const int MAX = 1e2;
int seq[MAX], n;
void solve(int cur){
	if(cur == n){
		for(int i = 1; i <= n; ++i) cout << seq[i] << " "; cout << endl;
		return;
	}
	map<int, int> sq;//key: 元素值, value: 元素在seq中下標 
	for(int i = cur; i <= n; ++i) sq[seq[i]] = i; 
	for(map<int, int>::iterator it = sq.begin(); it != sq.end(); ++it)
		swap(seq[cur], seq[it->second]), solve(cur + 1), swap(seq[cur], seq[it->second]);
}
int main(){
	scanf("%d", &n); for(int i = 1; i <= n; ++i) seq[i] = i;
	solve(1);
	return 0;
}