實際工作中怎麼驗證程序寫對了？

那些自己編程序實現比較複雜演算法的程序員如何去驗證自己的代碼是正確的？

如果用一組數據測試的話，那麼測試數據不也是是另一個程序算出來的嗎？如果這種演算法還沒有現成的程序，那麼如何產生測試數據？

舉例：對某種飛機的設計編程進行模擬，其中涉及的方程非常複雜，輸入輸出也非常多。很難用手工算出一組輸入數據對應的正確的輸出數據是什麼，那麼如何驗證編好的程序的輸出的模擬結果是正確的？

---

從嚴格到寬鬆，順序大概是：

1. 形式驗證，寫 Proof；
2. Property-based test；
3. 傳統單元測試。

寫 proof，在 Coq/Agda/Idris/F* 中可以直接做到，其他語言也有相關工具（好像 @張震 就寫了一個）。

而且如果真的有需求，這麼干也不是不可理喻的事情。比如編譯器的正確性就十分重要，然後就出現了 CompCert，一個經過嚴格形式化驗證的、正確的 C 編譯器。

例子：考慮一個簡單的程序——在數組中檢索元素，返回下標或者不存在（源：Main.idr）：

findIndex : DecEq a =&> Vect n a -&> a -&> Maybe (Fin n)
findIndex x [] = Nothing
findIndex x (y :: xs) =
case decEq x y of
Yes _ =&> pure FZ
No _ =&> [| FS (findIndex x xs) |]


怎麼說他是正確的呢？寫個命題：

findIndexOk : DecEq a =&> (x : a) -&> (xs : Vect n a) -&>
case findIndex x xs of
Just i =&> Elem x xs
Nothing =&> Not (Elem x xs)


然後證明出來

notHeadNotTail : Not (x = y) -&> Not (Elem x xs) -&> Not (Elem x (y :: xs))
notHeadNotTail notHead notTail Here = notHead Refl
notHeadNotTail notHead notTail (There tl) = notTail tl

findIndexOk : DecEq a =&> (x : a) -&> (xs : Vect n a) -&>
case findIndex x xs of
Just i =&> Elem x xs
Nothing =&> Not (Elem x xs)
findIndexOk x [] = absurd
findIndexOk x (y :: xs) with (decEq x y)
| Yes Refl = Here
| No notHead with (findIndexOk x xs)
| ih with (findIndex x xs)
| Nothing = notHeadNotTail notHead ih
| Just z = There ih


次嚴格的是用 PBT，刷一堆測試數據比較，它對於性質的約束也類似於命題，但採用傳統的布爾值，可以在更多程序語言中直接實現。

然後是普通的單元測試。

---

除了用 Coq 之類依賴類型語言寫證明以外，也可以用 SPIN/NuSMV 之類的 model checker 來寫 model，然後全自動驗證，當然能夠驗證的屬性局限在後端的 SMT solver （一般是 Z3）decidable 的 first order 屬性。工業界里 model checking 的應用更加廣泛一些（尤其涉及硬體/嵌入式開發）。

---

形式化一點的，有定理證明、模型檢查、抽象解釋（程序分析也能以驗證目標）。然後是各種程序測試。

對基於Coq/Isabelle 等工具的互動式驗證現狀不太了解。。而對於比較複雜的演算法和語言特性，自動化驗證的發展是很有限的，比如純數值程序的非線性循環不變式推導，大概21世紀才發展起來；涉及tree/graph的垃圾回收DSW演算法，06年才可以自動驗證[1]；如今風風火火的軟體模型檢查，也只是處理一些小程序、驗證些簡單的屬性[2]； 更有很多人已經不再verification, 跑去玩synthesis啦，就像當年compiler的一群人轉行verification 。。 總之，實際工作中還是老老實實寫測試、打log、printf吧（

[1] Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm, SAS 06

[2] 6th International Competition on Software Verification

---

絕大部分時候，只能迭代驗證。也就是一開始提一組數據，測試，通過的話再來新數據。這樣一直迭代下去。這麼做，沒法的出這個東西對不對，只能得出在一個既定的範圍內對不對。如果需要更嚴格的再用其他驗證方式。

---

我擦， 問題描述里原來不是有NS方程的么， 誰把問題描述去掉了， 搞得我像是在強答CS問題一樣。

======原答案==========

前面的大神都是從計算機理論， 形式證明的角度給出的答案， 我這裡想從科學計算角度來給出一個解答。

最近在寫畢業論文， 正好要介紹一段關於數值程序的驗證問題， 已經有很多答主提到了單元測試， 這裡講一下大規模數值模擬軟體的集成測試和定標（benchmark， 不知道怎麼翻譯）。

數值模擬軟體的一大特點決定了他們不太可能被精準的驗證， 很多非線性問題本身就沒有很好的解析解， 所以數值模擬是探索未知的過程， 正所謂智商不足程序湊。 這也就導致了一個很尷尬的情況： 我不知道我算出來的究竟是New Physics還是bug。極端的例子比如CFD領域的普惠PW6000設計事故（ 普惠PW6000的設計事故 - 航空高可信CFD活動論壇 - 流體論壇 - Powered by Discuz! ）。

目前計算流體領域以及彈性力學在程序驗證方面走在前列， 主要是因為其應用領域更貼近實際， 同時對結果的可信性要求比較高， 比如數值模擬程序驗證方面的論文很多都是武器實驗室發的。

主要的測試方法包括：

1. property based 比如驗證解的對稱性、解的趨勢
2. 簡單情況下的解析解/經典算例（golden case）
3. 對照已有的程序結果（。。。。都已經有了還要你何用。。。）
4. 精確解（Method of Exact Solution）方法， 與經典算例方法類似。
5. 構造解（Method of Manufactured Solutions）方法。

目前構造解方法被認為是能夠精確測試數值程序正確性以及演算法精度的一種方法。

簡單來說一個程序求解的（偏微分/微分積分）方程假設可以寫為

我們不知道在一個複雜區域內f的解。一種方法是使用簡單模擬區域和邊界條件解析求解， 然後跟數值結果對比（經典算例方法）。 另一種是人為指定一個複雜但是可以解析表示的模擬區域， 同時指定一個可以解析表示的 ， 然後強行修改governing equation， 將其變為

這樣就生生用解析的邊界條件和求解區域，構造出了一個新的方程。 而構造解 是滿足這一方程的。於是我們就可以把初值條件和邊界條件一設， 帶入新方程， 愉快的觀察數值解跟構造解之間的差別了。 如果使用的好， 可以直接測定出時間積分器的階數。

---

黑箱式的是最好調的，寫個隨機數據生成器，再手出幾個邊角數據就行。至於生成器，不需要很複雜，按照輸入規範來生成就好。隨機的地方就完全隨機，特定的地方就用列表隨機。

至於其它的，保證沒錯的辦法就是單步調試時輸出每一個變數並和自己計算出來的進行比對，當然這樣在程序複雜時根本就不科學。所以最好的辦法還是在寫的時候就盡量避免bug，然後自己或者找些其他人幫忙各種實際使用測試。

就算這樣也不能避免bug的出現，所以就有了版本這種東西（逃

---

比較實際的方法是學習和採用標準的單元測試方法，利用現有的單元測試框架，對自己開發的模塊進行足夠的單元測試，通常可以解決相當比例的缺陷。

除非代碼極其簡單，否則無法證明不存在缺陷。

測試只能證明代碼存在問題，無法證明代碼不存在問題。

---

好問題，基於實際工作講一點體會。

首先要判斷自己寫的演算法在功能方面是此前已經有的，還是新創造的。

如果是此前已有的，那麼相對可靠的實現作為benchmark. 舉個例子，假設你發明並且實現了一種排序演算法，先要根據對問題的理解生成足夠的未排序數據案例，這裡的足夠不止是數量，還包括不同的數據分布形態。然後，找個標準庫的排序演算法實現，用這個參考實現對每個測試案例做排序，最後和你自己寫的程序對比就可以了。

如果是前無古人的功能，第一要想辦法看能不能拆成若干個子功能，每個子功能找到測試參考。如果拆分下來仍然是前無古人的，那就只能根據問題本身設計測試例，所謂設計包括輸入數據，也包括預期輸出。一般來說寫全新功能本身就意味著對這個功能有充分的認識，寫代碼之前就能設計出測試例。

其次，是不是上述測試通過就說明沒bug了呢？不一定。測試例覆蓋的場景總是有限的，昨天在辦公室還聽到一個故事，某持續使用了30年的系統發現了一個bug，要知道此前可是有海量的測試。怎麼解決？我此前一份工作中有個土辦法，統計測試例的代碼覆蓋率，具體的說，現有測試例到底測到了代碼的哪些部分，還有哪些代碼完全沒執行過。針對後一種代碼，設計專門測試例。原理說起來簡單，但對於大型商業軟體做起來並不容易，主要是人力和時間開銷很大。實際上總是在最低代價滿足交付要求和儘可能查出bug之間找平衡。

---

寫個演算法

寫個暴力

寫個測試數據生成器

寫個腳本

不斷的把演算法和暴力的運行結果比較

這叫對拍 oier 都是這麼做的

---

1. 設計輸入數據來測試程序

• Statement testing: 保證每個statement都被執行至少一次
• Path testing: 每個logic path都被測試一遍

P.S. 基本僅適用於小型程序，如下，需4次pass才能cover所有logic paths：

if (condition1)
statement1;
else
statement2;

if (condition2)
statement3;
else
statement4;


大型程序之中的邏輯組合複雜，一般測試代碼片段

• Boundary testing (corner cases): 在domain邊界進行測試，如array首尾，matrix邊緣
• Stress testing: 突破限制外的測試，數據量要求大，variety要求高，通常為避免human bias採用程序隨機生成數據

2. 程序內的自我測試(assert)

• Validate parameters: 在函數的開頭驗證parameter是valid的
• Invariants: 在函數的開頭 assert(isValid(obj)) 驗證數據結構是valid的（如有必要，結尾也做一遍）
• Function return values: 檢查某些函數的return value，例如

if (scanf("%d%d", x, y) != 2)
/* Error handling code */


• Boundary cases： 同上
• 別刪testing code! 可以comment掉，或者用#ifdef...#endif和gcc -D之類的來disable，之類之類，但是別刪了！萬一以後還要用呢

3. 泛泛的blah blah之談

• 寫scripts
• 寫一點，測試一點，寫一點，測試一點……不要全部寫完再測試
• Regression testing: 有時候，運氣太差，可能修好一個bug，之前好好的部分，又被玩壞掉了 所以每次修好某bug，全部test cases都要重新測試一遍（寫scripts的另一個原因之一，若是全部手動測試，效率太低）
• 故意弄出一個bug，測試一下測試程序本身能不能捕捉到這個bug
• 讓別的生物（主要是程序員，程序猿和普通人類，其他例如計算咕咕雞，國利狗，蛤，李大貓，異形）來測試，少一些(報道上的)偏差

---

只能反覆測試，技術再好，經驗再豐富的coder也不可能寫出完全無bug的程序。只有經過各方面的測試。常見的測試有下面幾種：

Unit測試，暴力測試，兼容性測試，壓力測試 ，上線測試(發布Beta版)

這裡主要大概講一下Unit測試：

Unit測試就是給定入口和出口，然後把入口附給程序，看得出的結果是否和出口一致。

比如你寫了一個求圓的周長的方法，你定義了半徑這個入口，那麼你可以自己定一個半徑，然後，先手動計算出結果。然後再通過你的程序計算，如果２個結果一致，即可作出初步的判斷。

Unit測試也不是100%正確的，取決於你對可能出現的結果判斷的嚴謹性。

最好的方式就是將程序對象化，將處理問題的每個步驟方法化，一個方法，盡量只處理一件事情。這樣可以提高Unit測試的準確性。

Unit測試只是發現錯誤的一種方法，不能100%判斷程序的正確與錯誤，因為錯誤可能會發生在你的預告計算，或者你藉助的第三方計算工具。

另外，即時Unit測試也通過了，也未必就是正確的程序。因為還會有效率問題，兼容性問題。

還有時效性，過了某個時期，可能程序就無法運行了。

當年的千年蟲問題，不知道讓多少偉大的程序和軟體走下歷史舞台。

---

我覺得是可以測試的。可以分為兩部分。

1、演算法：這個是純數學方面的演算法，可以通過數學方面的推倒，確保演算法無誤。

2、代碼：既然樓主已經說了，這部分代碼是實現的一個非常複雜的數學邏輯，那麼，從數學的層面來看，一個複雜的數學公式和演算法，都是可以一步一步通過簡單的步驟推導而成。每一步都是可以比較容易的判斷是否是正確。（否則的話，在推導過程中，就無法保證是否是正確的。）

那麼事情就變得比較簡單了，既然放在一起比較難測試，那麼就用白盒單元測試，對實現這個演算法的每一步小的推導都可以做測試，這個是比較容易實現而且比較容易判斷正誤的。

然後既然整個演算法的每一步推導是正確的，每一步推導的代碼實現是正確的，那麼整個演算法的結果必然是正確的。

---

很難驗證自己的程序是完全正確的。。。 但是找到一個bad case就可以是錯的。類似於數學證明吧

---

簡單講，就是測試加分析

---

完全測試是不可能的，只能在條件允許的情況下儘可能減少錯誤概率

---

推薦閱讀：