點此開啟題目頁面

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

//CH0302_遞迴實現組合型列舉
#include <iostream>
#include <cstdio>
#include <vector>
using namespace std;
int n, m;
vector<int> choosn;
void solve(int cur){
	if(choosn.size() + (n - cur + 1) < m) return;
	if(choosn.size() == m){
		for(int i = 0; i < m; ++i) cout << choosn[i] << " "; cout <<endl;
		return;
	}
	choosn.push_back(cur), solve(cur + 1), choosn.pop_back();
	solve(cur + 1);
}
int main(){
	scanf("%d %d", &n, &m); 
	solve(1);
	return 0;
}
 

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

定義集 = { x | x為一次solve(i)的呼叫執行, 滿足進入呼叫後的初始choosn[0...choosn.size() - 1]嚴格遞增且對應{1,...,i - 1}的一個子集且choosn.size() <= m }

    歸納起點: 對於中的元素a, 根據程式碼邏輯易知, 設集S(可能為空)為當前choosn對應集合和集{n}的所有子集的並集構成的集合, 若S中不存在基數為m的集合, 那麼程式直接放回上級呼叫者, 否則程式按照字典序遞增的方式列印S中所有基數為m集合, 並且每個集合按照元素遞增列印在單獨行. 

    遞推: 假設對於(2 =< k <= n)中的元素上述結論成立, 容易證明其對於中的元素也是成立的

    綜上述, 對於中的元素上述結論成立, 從而程式正確性的得證