HarmonyOS开发者限时福利来啦!最高10w+现金激励等你拿~ 了解详情
写点什么

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

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

关注

评论

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

多平台小程序一站式管理工具推荐~

Geek_2305a8

实例带你了解GaussDB数据库的LOCK TABLE

华为云开发者联盟

数据库 后端 华为云 华为云GaussDB 华为云开发者联盟

机器人装行业MES/低代码平台免费使用/低代码MES

万界星空科技

低代码 低代码平台 mes 万界星空科技 机器人组装

图数据库基准测试 LDBC SNB 系列讲解:Schema 和数据生成的机制

NebulaGraph

图数据库 LDBC

ICP Rust CDK|IC和Rust简介

TinTinLand

学习 黑客 编程语言 web3 ICP

一文让你知道,云计算环境下云管平台的重要性

行云管家

云计算 云服务 云管平台 云资源

发布DDD脚手架到Maven仓库,IntelliJ IDEA 配置一下即可使用

EquatorCoco

Java DDD IDEA

2024 年 2 月 NFT 行业动态:加密货币飙升,NFT 市场调整

Footprint Analytics

blockchain NFT NFT链游

网络安全AI智能体公司「云起无垠」获数千万元天使+轮融资,致力于大模型与网络安全深度融合的技术研究

云起无垠

火山引擎“数据飞轮”助力哪吒汽车智能创新

Geek_2d6073

探索PyTorch:介绍及常用工具包展示

霍格沃兹测试开发学社

深度!10个头脑风暴必备的模板,让脑暴更高效和富有成效!

彭宏豪95

思维导图 头脑风暴 在线白板 在线协作 效率软件

ICP Rust CDK|课程介绍

TinTinLand

学习 黑客 编程语言 #Web3 ICP

微信小程序管理软件助力企业数字化转型

Geek_2305a8

RDS for MariaDB“智能DBA助手”,让运维效率嗖嗖地!

华为云开发者联盟

数据库 后端 华为云 华为云开发者联盟

深入理解位运算符及其在JavaScript中的应用

Immerse

学编程前需要知道哪些编程语言呢?

小齐写代码

WebRTC构建点对点的即时通讯工具

鲸品堂

工具 企业号 3 月 PK 榜

印刷行业实施MES管理系统有哪些重要的意义

万界星空科技

工业互联网 制造业 mes 印刷行业 万界星空科技

充电桩组装行业生产管理MES系统解决方案

万界星空科技

制造业 生产管理系统 mes 充电桩 汽车充电桩

为多渠道销售集成商品API接口

Noah

2024年值得尝试的22款在线管理软件盘点!

爱吃小舅的鱼

项目管理软件 项目管理x

有点害怕,浏览器插件风险这么多?

高端章鱼哥

新一代实时数据集成框架 Flink CDC 3.0 —— 核心技术架构解析

Apache Flink

Python 初学者容易踩的 5 个坑

不在线第一只蜗牛

Java Python 开发语言

通过统一规划和团队整合,提升企业财务洞察

智达方通

全面预算管理 财务洞察

Vue3 - 表单的输入与绑定

霍格沃兹测试开发学社

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