如何證明實現的演算法和數據結構是正確的？

01-05

比如各種複雜的樹，各種複雜的圖演算法什麼的，單單只靠測試用例的話感覺沒法做到完備，又或者只能通過Precondition+Invariant來推導Postcondition，在複雜的實現中是否真的可行？

演算法導論有些地方講了複雜度+正確性證明。另外推薦一本書，算是介於理論和實踐之間：

The Science of Programming (豆瓣) 。很理論又好上手的書，，還是算了。

實際開發中，主要用各種測試方法。當然測試技術在工業、學術界也是在不斷進步的。

面試中，被問道演算法正確性，用自然語言講講就夠了，反證法、數學歸納法用得比較多。

學術上的，搜a verified implementation of，certified software，model checking, hoare logic...有真相。。目前最大型成功的可能要屬 http://sel4.systems/ 了（已開源）。工具嘛，可能會用Coq, Isabella, Agda（它們都有Curry Howard Isomorphism的魂， dependent type的形。。）

不知道題主的具體需求是什麼。。

樓主你知道霍爾邏輯嗎？

一種方法是使用Coq。

例：

Sylvain Conchon and Jean-Christophe Filliatre. 2007. A persistent union-find data structure. InProceedings of the 2007 workshop on Workshop on ML (ML "07). ACM, New York, NY, USA, 37-46. DOI=10.1145/1292535.1292541 A persistent union-find data structure

一般來說，如果是測試這種複雜的演算法的話，我們要求組合覆蓋。也就是說，你的代碼裡面每一次if都有兩個選擇，你把所有的組合都過一遍，如果沒問題，就姑且當他沒問題了。

去acm上以a verified implementation of為關鍵詞搜幾篇文看看不就明白了。

Oregon Programming Languages Summer School

看Appel那部分的lecture

對於足夠複雜的問題來說，理論上你只能盡量逼近，通常無法做到證明其正確性，也無法證明代碼是 bug-free 的。比如非常依賴外部事件時序的調度演算法，或不同實體(線程/進程/cluster)間密集的資源共享。

當然了，如果能做到從數學模型到代碼的完美映射，然後證明數學模型的正確性和完備性，理論上是能產生完全正確的代碼的。然而實際上往往做不到這一點，這也是編程(programming)通常被認為是一種工程(engineering)活動的原因。

CMU 15122 Principles of Imperative Computation

Contracts

http://www.cs.cmu.edu/~rjsimmon/15122-f14/schedule.html

遞歸：數學歸納法

迭代：每一次狀態轉移，只要能把問題規模縮小，這個演算法就是對的（算是簡化的數學歸納法），縮小的速度決定時間複雜度

Coq