BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

Spec#与Boogie发布于CodePlex

| 作者 Jonathan Allen 关注 614 他的粉丝 ,译者 王波 关注 0 他的粉丝 发布于 2009年8月11日. 估计阅读时间: 1 分钟 | CNUTCon 了解国内外一线大厂50+智能运维最新实践案例。

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

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我
社区评论

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT