快手、孩子王、华为等专家分享大模型在电商运营、母婴消费、翻译等行业场景的实际应用 了解详情
写点什么

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

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

关注

评论

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

python 无监督生成模型

快乐非自愿限量之名

Python 开发语言 监督

融云上线 HarmonyOS NEXT 版 SDK,全面适配「纯血鸿蒙」生态

融云 RongCloud

什么是客户体验自动化?

快乐非自愿限量之名

运维 自动化 低代码 客户体验

这2个AI格式转换工具,轻松将PDF文件转为PPT!

彭宏豪95

人工智能 效率工具 格式转换 AIGC AI生成PPT

GitHub高赞!Python零基础也能搞定的数据分析与处理

我再BUG界嘎嘎乱杀

Python 数据分析 Excel 数据处理 开发语言

《中国数据库系列纪录片》轻舟已过万重山

不惑

数据库 历史 国产数据库

助力游戏实现应用内运营闭环,融云游戏社交方案升级!

融云 RongCloud

融云 CEO 董晗获颁 EqualOcean「2024 出海全球化服务 30 人」

融云 RongCloud

观测云赋能「阿里云飞天企业版」,打造全方位监控观测解决方案

观测云

监控

idm不能续传是什么意思 idm无法继续下载文件 IDM的断点续传功能 IDM是什么软件

禁止废话

断点续传 网络加速 下载器 IDM idm下载

阿里巴巴关键字搜索商品API返回值解析:电商数据驱动的电商运营流程优化

技术冰糖葫芦

API Explorer API 编排 API 安全 API 文档

基于低代码开发技术的管理会计体系架构研究

EquatorCoco

架构 低代码 系统开发

企业供应链数字化的挑战与应对:转型之路的技术破解

不在线第一只蜗牛

低代码 数字化 供应链

服务端性能测试:行业流行性能压测工具介绍

测吧(北京)科技有限公司

测试

鸿蒙,我们土地上开出的花

脑极体

AI

idm支持断点续传吗 idm断点续传如何使用

禁止废话

网络加速 下载器 大文件断点续传 idm下载 网页视频下载工具

豆瓣评分9.5!清华大牛熬夜整理的Python深度学习教程开发下载!

我再BUG界嘎嘎乱杀

Python 人工智能 深度学习

淘宝商品详情数据(实时更新,缓存数据)

tbapi

淘宝商品详情数据接口 淘宝API 淘宝商品数据采集

和小红书一起参会! 了解大模型与大数据融合的技术趋势

小红书技术REDtech

数据 会议 大模型

京东JD商品sku信息API返回值探索:商品规格数据与跨境电商机遇

技术冰糖葫芦

API Explorer API 编排 API 安全 API 文档

搜索型数据库的技术发展历程与趋势前瞻

极限实验室

趋势 搜索型数据库

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