点此打开题目页面

先给出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;
}