Spec# 与 Boogie 发布于 CodePlex

阅读数:750 2009 年 8 月 10 日

话题:.NET语言 & 开发架构文化 & 方法

Spec#是一种基于 C# 的研究型语言。它是基于契约优先的原则,即函数的前提条件和后置条件都以声明的方式定义。其他的特性还包括类不变量、非空引用类型和加强的静态分析功能。

我们可以在.NET 4 中找到一些重要的特性,比如:代码契约,Spec# 当前的研究状况比较尴尬。最近,微软声明放宽对它的约束,但也仅是一点而已。获取了微软研究共享许可协议后,Spec# 的源代码已经可以从 CodePlex 站点上下载了。这份许可仅限于非商业用途。

与 Spec# 配套的有 Boogie,一种用于代码验证的中间语言。Boogie 并非仅限于.NET,它还支持其他的语言,包括“HAVOC、C 语言的验证程序 vcc、Dafny 语言和它的验证程序以及并发语言 Chalice”。

Boogie 还是一种工具的名称。该工具接受 Boogie 语言的输入,并随意地推断给定 Boogie 程序的一些不变量,接着生成验证条件,然后传给 SMT 解算程序。默认的 SMT 解算程序是 Z3。

Boogie 已经基于微软公共许可正式发布,它符合开源标准。

当前微软把代码契约定位为今后的发展方向,这意味着 Spec# 未来很可能不会有太大的发展。

查看英文原文:Spec# and Boogie Released on CodePlex