免费下载案例集|20+数字化领先企业人才培养实践经验 了解详情
写点什么

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

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

关注

评论

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

PCB阻焊桥存在的DFM(可制造性)问题,华秋一文告诉你

华秋电子

Viu联合华为HMS生态,共创影音娱乐新体验

HarmonyOS SDK

HMS Core

助力春耕:数智驱动现代农业高质量发展

加入高科技仿生人

数字化 农业 数智化 农业农村数字化

从零到跑通TPC-H:如何快速实现查询计划

MatrixOrigin

分布式数据库 MatrixOrigin MatrixOne TPC-H

百度智能云亮相CCBN 2023,共拓媒体数智化转型新征程

Geek_2d6073

超强版干货投递!Milvus 的部署心得、运维秘籍都在这里了!

Zilliz

Milvus Zilliz ChatGPT LLM zillizcloud

2023年全互联网最新版Java面试突击手册PDF版开源,押题率高达97%

开心学Java

Java 面试 java; 八股文 Java八股文

4 月 25 日直播预告 | 深入解读 Flink 1.17

Apache Flink

大数据 flink 实时计算

GitHub星标48k!蚂蚁金服开源的这份SpringBoot笔记

做梦都在改BUG

Java spring Spring Boot 框架

macOS下快速复制文件或文件夹路径的技巧

互联网搬砖工作者

OneNote 2019 for Mac 中文版附激活工具

真大的脸盆

Mac Mac 软件 笔记应用

保险行业如何将质检覆盖率从5%提升至100%?

中关村科金

保险 智能质检

CSS奇思妙想之-利用CSS裁剪(clip-path)完成各种图形

肥晨

三周年连更

面试官:Redis有什么持久化策略?

做梦都在改BUG

Java redis 缓存 面试 持久化

多元融合成为音视频技术发展新风向

中关村科金

实时音视频 监管合规

云上数据变革:Databend Cloud 正式发布

Databend

即时通讯系统为什么选择GaussDB(for Redis)?

华为云开发者联盟

数据库 后端 华为云 华为云开发者联盟 企业号 4 月 PK 榜

数据中台建设:千万级的瀑布式,和十万级的迭代式,你会选择哪一个?

tapdata

中台 服务化 Tapdata DaaS 现代数据栈

【网易云信】网易云信 RTC 音频 QoS 综述

网易智企

RTC 实时音视频

免费领取 | ONES 联合中国信通院发布《中国企业软件研发管理白皮书》

万事ONES

AIGC的阿克琉斯之踵

华为云开发者联盟

人工智能 AI 华为云 华为云开发者联盟 企业号 4 月 PK 榜

10万字干货:《数字业务连续性提升最佳实践》免费领取|TakinTalks社区

TakinTalks稳定性社区

微服务 - 注册中心和配置中心(Consul)

做梦都在改BUG

Java 微服务 注册中心 配置中心

景区共享电单车如何投放?投放意义?

共享电单车厂家

共享电动车厂家 景区共享电单车 共享电单车投放

阿里大牛纯手写的微服务入门笔记,从基础到进阶直接封神

做梦都在改BUG

Java 微服务 spring cloud alibaba

物联网常见协议之Amqp协议及使用场景解析

华为云开发者联盟

后端 物联网 华为云 华为云开发者联盟 企业号 4 月 PK 榜

PCB生产工艺 | 第十三道主流程之包装

华秋电子

连接 1 次孤岛,服务 N 个场景(报名中)

tapdata

DaaS

MLCC是电子工业大米,供需波动导致行业成周期性波动

华秋电子

即时通讯技术文集(第13期):Web端即时通讯技术精华合集 [共15篇]

JackJiang

网络编程 即时通讯 IM

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