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

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

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

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

Boogie已經基于微軟公共許可正式發布，它符合開源標準。

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

【編輯推薦】

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