談程序的正確性

文/王垠

不管在學術圈還是在工業界，總有很多人過度的關心所謂“程序的正確性”，有些甚至到了戰戰兢兢，舍本逐末的地步。下面舉幾個例子：

• 很多人把測試（test）看得過于重要。代碼八字還沒一撇呢，就吵著要怎么怎么嚴格的測試，防止“將來”有人把代碼改錯了。這些人到后來往往被測試捆住了手腳，寸步難行。不但代碼 bug 百出，連測試里面也很多 bug。

• 有些人對于“使用什么語言”這個問題過度的在乎，仿佛只有用最新最酷，功能最多的語言，他們才能完成一些很基本的任務。這種人一次又一次的視一些新語言為“靈丹妙藥”，然后一次又一次的幻滅，最后他們什么有用的代碼也沒寫出來。

• 有些人過度的重視所謂“類型安全”（type safety），經常抱怨手頭的語言缺少一些炫酷的類型系統功能，甚至因此說沒法寫代碼了！他們沒有看到，即使缺少一些由編譯器靜態保障的類型安全，代碼其實一點問題都沒有，而且也許更加簡單。

• 有些人走上極端，認為所有的代碼都必須使用所謂“形式化方法”（formal methods），用機器定理證明的方式來確保它 100% 的沒有錯誤。這種人對于證明玩具大小的代碼樂此不疲，結果一輩子也沒寫出過能解決實際問題的代碼。

100% 可靠的代碼，這是多么完美的理想！可是到最后你發現，天天念叨著要“正確性”，“可靠性”的人，幾乎總是眼高手低，說的比做的多。自己沒寫出什么解決實際 問題的代碼，倒是很喜歡對別人的“代碼質量”評頭論足。這些人自己的代碼往往復雜不堪，喜歡使用各種看似高深的奇技淫巧，用以保證所謂“正確”。他們的代 碼被很多所謂“測試工具”和“類型系統”捆住手腳，卻仍然 bug 百出。到后來你逐漸發現，對“正確性”的戰戰兢兢，其實是這些人不解決手頭問題的借口。

衡量程序最重要的標準

這些人其實不明白一個重要的道理：你得先寫出程序，才能開始談它的正確性。看一個程序好不好，最重要的標準，是看它能否有效地解決問題，而不是 它是否正確。如果你的程序沒有解決問題，或者解決了錯誤的問題，或者雖然解決問題但卻非常難用，那么這程序再怎么正確，再怎么可靠，都不是好的程序。

正確不等于簡單，不等于優雅，不等于高效。一個不簡單，不優雅，效率低的程序，就算你費盡周折證明了它的正確，它仍然不會很好的工作。這就像你 得先有了房子，才能開始要求房子是安全的。想想吧，如果一個沒有房子的流浪漢，路過一座沒有人住的房子，他會因為這房子“不是 100% 安全”，而繼續在野外風餐露宿嗎？寫出代碼就像有了房子，而代碼的正確性，就像房子的安全性。寫出可以解決問題的程序，永遠是第一位的。而這個程序的正確 性，不管它如何的重要，永遠是第二位的。對程序的正確性的強調，永遠不應該高于寫出程序本身。

每當談起這個問題，我就喜歡打一個比方：如果“黎曼猜想”被王垠證明出來了，它會改名叫“王垠定理”嗎？當然不會。它會被叫做“黎曼定理”！這 是因為，無論一個人多么聰明多么厲害，就算他能夠證明出黎曼猜想，但這個猜想并不是他最先想出來的。如果黎曼沒有提出這個猜想，你根本不會想到它，又何談 證明呢？所以我喜歡說，一流的數學家提出猜想，二流的數學家證明別人的猜想。同樣的道理，寫出解決問題的代碼的人，比起那些去證明（測試）他的代碼正確性 的人，永遠是更重要的。因為如果他沒寫出這段代碼，你連要證明（測試）什么都不知道！

如何提高程序的正確性

話說回來，雖然程序的正確性相對于解決問題，處于相對次要的地位，然而它確實是不可忽視的。但這并不等于天天鼓吹要“測試”，要“形式化證明”，就可以提高程序的正確性。

如果你深入研究過程序的邏輯推導就會知道，測試和形式化證明的能力都是非常有限的。測試只能測試到最常用的情況，而無法覆蓋所有的情況。別被所 謂“測試覆蓋”（test coverage）給欺騙了。一行代碼被測試覆蓋而沒有出錯，并不等于在那里不會出錯。一行代碼是否出錯，取決于在它運行之前所經過的所有條件。這些條件 的數量是組合爆炸關系，基本上沒有測試能夠覆蓋所有這些前提條件。

形式化方法對于非常簡單直接的程序是有效的，然而一旦程序稍微大點，形式化方法就寸步難行。你也許沒有想到，你可以用非常少的代碼，寫出 Collatz Conjecture 這樣至今沒人證明出來的數學猜想。實際使用中的代碼，比這種數學猜想要復雜不知道多少倍。你要用形式化方法去證明所有的代碼，基本上等于你永遠也沒法完成項目。

那么提高程序正確性最有效的方法是什么呢？在我看來，最有效的方法莫過于對代碼反復琢磨推敲，讓它變得簡單，直觀，直到你一眼就可以看得出它不可能有問題。