這周我讀了《軟件工程——實踐者的研究方法》，這是一本比較理論的書，看起來略有一些乏味。其中談到很多項目質量管理，開發模式相關的東西，感覺都太泛泛了。因為比較缺乏實戰經驗，書中又很少講實際例子，因此這些內容並沒有給我留下太多印象。
但書中花了好幾章的篇幅用於講軟件測試，這部分內容我很感興趣。如何開發出沒有bug 或 bug 很少的程序一直我想探究的問題。PL 領域有很多相關的研究用於保證程序正確性和代碼質量，例如：模型檢查、程序分析、程序證明等。這些方法代價太高，一般只用於十分重要的工程中，例如核反應堆控制系統，動車控制系統等。普通的軟件工程很難用到這些方法。
對於普通軟件工程來說，測試是很好的保障軟件正確性的方法。測試的種類有很多，有單元測試、回歸測試、壓力測試、alpha 測試、beta 測試等。不同的測試的側重點不一樣，有的是針對軟件安全性，有的是針對軟件正確性，有的是針對軟件易用性。
在看了這些軟件工程的書之后，我對保證軟件正確性這個問題有了一些新的想法。在程序中，類型可以用來約束程序行為，保證函數調用是安全的。但目前的類型只是描述了這個東西是什么，卻很少有關於這個東西性質的描述。例如在 Int 類型，只描述了它是整數類型，而這個整數類型具體映射到解空間是什么東西，卻沒有涉及。它可以是一個計數器，可以是一個素數，可以是一個年份等等。而且，這些具體在解空間中的語義，有時候還有一些約束條件，例如：計數器通常需要是正數，素數必須滿足定義等。在程序驗證中，這種類型叫做 “精化類型” (refinement type)。但是學術界用這種方法，通常是用來表示霍爾邏輯，並且交給 SMT Solver 進行約束求解，這種基於驗證的方法前面已經提到，代價太昂貴。
因此，我們可以用測試、運行時斷言來保證精化類型的約束滿足。