AICon 上海站|90%日程已就绪,解锁Al未来! 了解详情
写点什么

Spec#与 Boogie 发布于 CodePlex

  • 2009-08-10
  • 本文字数:467 字

    阅读完需:约 2 分钟

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

2009-08-10 04:241684
用户头像

发布了 87 篇内容, 共 22.6 次阅读, 收获喜欢 1 次。

关注

评论

发布
暂无评论
发现更多内容

Snowflake vs. Databricks谁更胜一筹?2022年最新战报

雨果

数据中台 数据平台 snowflake DaaS数据即服务 Databricks

OpenAtom OpenHarmony分论坛,今天14:00见!附大事记精彩发布

OpenHarmony开发者

OpenHarmony

Java 多商户外贸版 PC 端功能,出场就是这么硬核!

CRMEB

《数字经济 科技向善》大咖对谈干货来啦

易观分析

金融科技

Redis总结:缓存雪崩、缓存击穿、缓存穿透与缓存预热、缓存降级

程序员啊叶

Java 编程 程序员 架构 java面试

Java——AOP案例之测量业务层接口执行效率

王小凡

Java 程序员 apo

以科技传递温度,vivo亮相数字中国建设峰会

极客天地

Seata 在蚂蚁国际银行业务的落地实践

SOFAStack

开源项目 seata 项目实践 多编程语言 蚂蚁国际

续上,Python爬虫在 fiddler 中调用本地 JS 代码文件

梦想橡皮擦

Python 爬虫 7月月更

数据分析如何解决商业问题?这里有份超详细攻略

博文视点Broadview

字节前端面试题总结

buchila11

前端面试

面试官常问:如何手撸一个“消息队列”和“延迟消息队列”?

程序员啊叶

Java 编程 程序员 架构 java面试

阿里P8熬了一个月肝出这份32W字Java面试手册,在Github标星31K+

程序员啊叶

Java 编程 程序员 架构 java面试

常见分布式理论(CAP、BASE)和一致性协议(Gosssip、Raft)

程序员啊叶

Java 编程 程序员 架构 java面试

YonBuilder赋能创新,用友第四届开发者大赛“金键盘奖”开启竞逐!

科技热闻

通过14个入门实战案例教大家快速学习Python编程语言

小院里的霍大侠

Python Python初学者 程序员‘ 编程入门 兴趣编程

程序员培训学习后好找工作吗

小谷哥

学习Java开发技术建议

小谷哥

腾讯云联合中国工联院发布工业AI质检标准化研究成果加速制造业智能化转型

科技热闻

初学者入门:使用WordPress搭建一个专属自己的博客

hum建应用专家

数据库 Wordpress 博客部署 WordPress

深入理解MySQL主从复制原理以及集群部署过程

jiangxl

MySQL 数据库 运维 dba 签约计划第三季

在web前端培训机构应该如何学习前端

小谷哥

es6 class 继承的重点

掘金安东尼

JavaScript 前端 ES6 7月月更

华硕无双,这可能是屏幕最好的平价高刷轻薄笔记本

科技热闻

什么是私域流量?

源字节1号

软件开发

Go语言系列:如何搭建Go语言开发环境?

小黑豆豆

后端 安装 教程 Go 语言 签约计划第三季

责任链模式在转转精准估价中的应用

转转技术团队

设计模式 责任链

2022 秋招 Java 岗面试高频问题总结

程序员啊叶

Java 编程 程序员 架构 java面试

WEB服务如何平滑的上下线

转转技术团队

nginx Java web

尚硅谷Elasticsearch8.X视频教程

小谷哥

web前端技术前景如何?

小谷哥

Spec#与Boogie发布于CodePlex_.NET_Jonathan Allen_InfoQ精选文章