10 月 23 - 25 日,QCon 上海站即将召开,现在购票,享9折优惠 了解详情
写点什么

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

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

关注

评论

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

翻译之深入注释俄罗斯民间故事的语料库,以实现对俄罗斯形式主义理论的机器学习

AI代笔

OpLog4j

Geek_746da6

百度人工智能OCR调用调试过程

tuuezzy

一线城市年轻人生活工作实录(程序员篇)

Marilyn

敏捷开发 开发者工具 快速开发

WSDM Cup 2020大赛金牌参赛方案全解析

华为云开发者联盟

大数据 搜索 信息

图扑软件联手阿里Lindorm数据库开启工业物联超融合存储模式

许力

IoT AIOT

年轻人大企打拼多年,刚升迁便遇巨大阻力难以解决,到底如何才能在职场中幸存?

Marilyn

敏捷开发 快速开发

华为云专家讲述知识图谱构建流程及方法

华为云开发者联盟

华为 数据 知识图谱

JVM-技术专题-类加载机制

码界西柚

Java JVM

亚马逊Prime会员日火爆开启一站购全球逾3000万正品商品

爱极客侠

微前端之如何拆解React巨石应用 qiankun

SugarTurboS

项目管理 架构 大前端 React

JVM-技术专题-Java类文件结构

码界西柚

Java JVM

国外的公司都是如何对待大龄程序员的?在国内该如何应对?

Java架构师迁哥

来喽,来喽,Python 3.9正式版发布了~~~

华为云开发者联盟

Python 编程

第三周作业一

dll

医疗AI系统构建(1)one-hot编码

刘旭东

人工智能 学习 医疗AI one-hot

Lindorm云原生数据库 - 让数字时代IT运维系统“灵动”起来

许力

DevOps APM Data Lake AIOPS

OKR-VUCA时代目标管理利器实践分享

张兆东

苦难过后,终会团聚

hellocj

JVM-技术专题-对象的实例化过程

码界西柚

Java JVM

高难度对话读书笔记—聆听篇

wo是一棵草

从哲学源头思考自动驾驶网络架构设计

华为云开发者联盟

自动驾驶 架构

Programmatic Navigation using SwiftUI| 使用SwiftUI进行程序化导航

Daniel

在线教育企业迎来“秋招”大考,数字用户体验成胜负关键手

博睿数据

运维 APM 在线教育 AIOPS 用户体验

我和我的智能联接

脑极体

图解 K8S 源码 - Informer 篇

郭旭东

Kubernetes Kubernetes源码

拜托,学妹,别再问我怎么自学 Java 了!和盘托出

沉默王二

Java 自学编程

LeetCode题解:94. 二叉树的中序遍历,使用栈,JavaScript,详细注释

Lee Chen

大前端 LeetCode

有了TA,领域外企业里的小IT团队,也能轻松搞定大型项目

Marilyn

敏捷开发 快速开发

The story of programmers in famous enterprises.

Marilyn

敏捷开发 快速开发

个人数字人民币钱包即将亮相

CECBC

央行 数字人民币

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