AICon 北京站 Keynote 亮点揭秘,想了解 Agent 智能体来就对了! 了解详情
写点什么

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:241766
用户头像

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

关注

评论

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

运维防背锅的办法之一:命令审计

蝉翼2u

程序员 运维 安全 开发 审计

ebay商品详情数据接口|ebay API接口指南

tbapi

ebay api ebay商品详情接口 ebay商品数据采集 易贝商品详情接口 易贝API

企业im是什么?

BeeWorks

企业级移动应用平台是什么?

BeeWorks

基于Java+SpringBoot+Vue健身俱乐部管理系统设计和实现

hunter_coder

后端开发

基于Java+SpringBoot+Vue桂林旅游景点导游平台设计和实现

hunter_coder

后端开发

XR实时云渲染-加速虚拟仿真云教学呈现!

3DCAT实时渲染

云渲染 虚拟仿真 实时云渲染 虚拟仿真云教学

IM即时通讯软件,企业即时通讯系统—WorkPlus

BeeWorks

基于业务规则拆分用户故事——避免工作局促

Bruce Talk

敏捷开发 Agile User Story

携程景点美食数据采集接口:连接用户与目的地的桥梁

tbapi

携程API 携程景点数据采集 携程美食数据采集 携程景点API 携程美食API

网络安全作业三

白开水又一杯

客户在哪儿AI与其他服务于B端的科技产品有何不同

客户在哪儿AI

人工智能 ToB营销 ToB增长 大客户营销

企业级im即时通讯可以给企业解决什么问题?

BeeWorks

1688商品详情数据接口|1688API接口指南

tbapi

1688 1688商品详情接口 1688API 1688商品详情数据接口

一个改行做程序员的老ToB市场人的心路历程

客户在哪儿AI

人工智能 ToB营销 ToB增长 大客户营销

基于Java+SpringBoot+Vue多媒体素材管理系统设计和实现

hunter_coder

后端开发

义乌购商品详情API接口:探索海量商品的深度信息

tbapi

义乌购商品详情数据接口 义乌购API 义乌购商品数据采集

基于Java+SpringBoot+Vue扶农助农政策管理系统设计和实现

hunter_coder

后端开发

基于Java+SpringBoot+Vue教学资源库设计和实现

hunter_coder

后端开发

基于Java+SpringBoot+Vue服装生产管理设计和实现

hunter_coder

后端开发

基于Java+SpringBoot+Vue狗粮销售商城系统设计和实现

hunter_coder

后端开发

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