Spec#是一種基于C#的研究型語言。它是基于契約優(yōu)先的原則，即函數(shù)的前提條件和后置條件都以聲明的方式定義。其他的特性還包括類不變量、非空引用類型和加強的靜態(tài)分析功能。

我們可以在.NET 4中找到一些重要的特性，比如：代碼契約，Spec#當前的研究狀況比較尷尬。最近，微軟聲明放寬對它的約束，但也僅是一點而已。獲取了微軟研究共享許可協(xié)議后，Spec#的源代碼已經(jīng)可以從CodePlex站點上下載了。這份許可僅限于非商業(yè)用途。

與Spec#配套的有Boogie，一種用于代碼驗證的中間語言。Boogie并非僅限于.NET，它還支持其他的語言，包括“HAVOC、C語言的驗證程序vcc、Dafny語言和它的驗證程序以及并發(fā)語言Chalice”。

Boogie還是一種工具的名稱。該工具接受Boogie語言的輸入，并隨意地推斷給定Boogie程序的一些不變量，接著生成驗證條件，然后傳給SMT解算程序。默認的SMT解算程序是Z3。

Boogie已經(jīng)基于微軟公共許可正式發(fā)布，它符合開源標準。

當前微軟把代碼契約定位為今后的發(fā)展方向，這意味著Spec#未來很可能不會有太大的發(fā)展。

【編輯推薦】

1. 新型動態(tài)編程語言Snow簡介
2. Google推出新編程語言Simple 用于Android開發(fā)
3. 微軟為SOA打造全新編程語言：D語言？
4. 淺析.NET平臺編程語言的未來走向
5. Erlang面向分布與并發(fā)的編程語言