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

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

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

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

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

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

【編輯推薦】

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