初探微軟研究型語言Spec#
作者：王波 譯
Spec#是一種基于C#的研究型語言。我們可以在.NET 4中找到一些重要的特性，比如：代碼契約,即函數的前提條件和后置條件都以聲明的方式定義。其他的特性還包括類不變量、非空引用類型和加強的靜態分析功能。
Spec#是一種基于C#的研究型語言。它是基于契約優先的原則，即函數的前提條件和后置條件都以聲明的方式定義。其他的特性還包括類不變量、非空引用類型和加強的靜態分析功能。
我們可以在.NET 4中找到一些重要的特性，比如：代碼契約，Spec#當前的研究狀況比較尷尬。最近，微軟聲明放寬對它的約束，但也僅是一點而已。獲取了微軟研究共享許可協議后，Spec#的源代碼已經可以從CodePlex站點上下載了。這份許可僅限于非商業用途。
與Spec#配套的有Boogie，一種用于代碼驗證的中間語言。Boogie并非僅限于.NET，它還支持其他的語言，包括“HAVOC、C語言的驗證程序vcc、Dafny語言和它的驗證程序以及并發語言Chalice”。
Boogie還是一種工具的名稱。該工具接受Boogie語言的輸入，并隨意地推斷給定Boogie程序的一些不變量，接著生成驗證條件，然后傳給SMT解算程序。默認的SMT解算程序是Z3。
Boogie已經基于微軟公共許可正式發布，它符合開源標準。
當前微軟把代碼契約定位為今后的發展方向，這意味著Spec#未來很可能不會有太大的發展。
【編輯推薦】
責任編輯：佚名
來源：
InfoQ
