写点什么

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

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

关注

评论

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

我们公司使用了6年的项目部署方案,打包 + 一键部署详解,稳的一批

沉默王二

Java

大数据培训Flink 流怎么来处理 API

@零度

flink 大数据开发

时序数据是如何被压缩的?具体有哪些可选择的压缩算法?

TDengine

数据库 tdengine 时序数据库

龙蜥社区成立云原生 SIG,引入 3 大核心技术,共建云原生生态

OpenAnolis小助手

开源 技术 云原生 龙蜥社区 sig

洞见科技助力华夏银行「隐私计算数据安全平台」建设,赋能金融业务提质增效

洞见科技

金融科技 隐私计算

SAP Marketing Cloud 功能概述(一)

汪子熙

云原生 SaaS SAP 6月月更 Marketing Cloud

Volcano社区v1.6.0版本正式发布

华为云开发者联盟

云计算 云原生 后端

华为云发布ModelBox AI应用开发框架

华为云开发者联盟

人工智能 华为云

软件开发外包的优势,哪些企业适合软件开发外包?

开源直播系统源码

软件开发 直播带货 直播带货源码 视频带货

征文投稿丨基于轻量应用服务器+OSS的中小型应用运维实践

阿里云弹性计算

运维 OSS CI/CD 轻量应用

Wallys/DR-AP6018-S-OUTDOOR/ IPQ6010/high power Radio AP

wallys-wifi6

IPQ4019 ipq6018

「势说新语」SBOM在企业软件供应链管理中的重要性—安全漏洞篇

安势信息

开源 漏洞 开源软件供应链 软件物料清单 SBOM

倒计时2日!基于 Apache DolphinScheduler&TiDB 的交叉开发实践,从编写到调度让你大幅提升效率

白鲸开源

Apache 大数据 开源 Apache DolphinScheduler

大数据系统包含哪些组件?需要过等保吗?

行云管家

大数据 数据 过等保

云渲染技术的“公”“私”

Finovy Cloud

服务器 云渲染 元宇宙 渲染器

5种在TypeScript中使用的类型保护

华为云开发者联盟

前端 变量 类型

im即时通讯的简介和趋势

BeeWorks

NodeJS 5分钟 连接 Redis 读写操作 👑

德育处主任

redis Node 6月月更

父亲节,这份孩子科学上网秘籍助你“爸”气全开

最新动态

Flink框架中的时间语义和Watermark(数据标记)

百思不得小赵

大数据 flink 6月月更

为什么不建议你用 MongoDB 这类产品替代时序数据库?

TDengine

数据库 tdengine 时序数据库

如何规避开源安全漏洞风险?新思科技OSSRA报告给出建议

BeeWorks

【Python技能树共建】常用标准库

梦想橡皮擦

Python 6月月更

SAP Field Service Management 和微信集成的案例分享和实现介绍

汪子熙

云原生 SaaS SAP 6月月更 Marketing Cloud

2022年秋季广州美博会-2022年9月份广州美博会

Geek_0b38bb

2022年广州美博会 秋季广州美博会 9月份广州美博会 美博会

2022年广州美博会-2022第60届广州国际美博会

Geek_0b38bb

2022年广州美博会 秋季广州美博会 美博会 第60届广州美博会

MySQL采用B+树作为索引的原因

龙空白白

索引结构 MySQL 数据库 索引原理

大数据培训Flink 中的 Window理解与分析

@零度

flink 大数据开发

ABAP-调用WebService服务

桥下本有油菜花

abap

记录那些年 Nacos 的坑

Damon

6月月更

2022年深圳美博会-2022年深圳国际美博会

Geek_0b38bb

美博会 2022年深圳美博会 2022年深圳国际美博会 深圳美博会

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