遞迴_CH0302_遞迴實現組合型列舉_遞迴演算法正確性證明範例
阿新 • • 發佈:2018-11-09
先給出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)中的元素上述結論成立, 容易證明其對於中的元素也是成立的
綜上述, 對於中的元素上述結論成立, 從而程式正確性的得證