AI实践哪家强?来 AICon, 解锁技术前沿,探寻产业新机! 了解详情
写点什么

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

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

关注

评论

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

2021年Android程序员职业规划,查缺补漏

android 程序员 移动开发

AndroidHook机制连简单实战都不会凭什么拿高薪,Android开发两年

android 程序员 移动开发

Android中高级面试必知必会,Android学习路线

android 程序员 移动开发

2021年阿里+腾讯+快手offer都已拿到,Android开发实战

android 程序员 移动开发

Android大厂面试真题解析大全,腾讯T3大牛手把手教你

android 程序员 移动开发

每秒创建百万文件,百度沧海·文件存储CFS推出新一代Namespace架构

百度开发者中心

架构 文件存储 cfs

997页手淘Android面试真题解析火爆全网,Android基础72问

android 程序员 移动开发

Activity的6大难点你会几个,面试复盘

android 程序员 移动开发

Android外包是如何转正网易的,大厂Android核心面试题出炉

android 程序员 移动开发

2021年Android社招面试题,薪资翻倍

android 程序员 移动开发

2021年安卓社招面试题精选,顺利拿到offer

android 程序员 移动开发

阿里云混合云Apsara Stack 2.0发布,加速政企数智创新

Lily

2021最新网易Android面试题目,2021Android架构面试指南

android 程序员 移动开发

42岁程序员面试,动脑学院vip课程百度云

android 程序员 移动开发

Android体系化进阶学习图谱,动脑学院课程值得买吗

android 程序员 移动开发

2021Android面试笔试总结!html5移动开发即学即用网盘

android 程序员 移动开发

2021大厂安卓知识点总结,字节跳动学习笔记

android 程序员 移动开发

2021金九银十,动脑学院官网

android 程序员 移动开发

Android开发入门教程!扔物线学堂

android 程序员 移动开发

Android开发岗还不会这些问题,15个经典面试问题

android 程序员 移动开发

分布式事务最经典的七种解决方案

Java 程序员 架构 面试 分布式

Android开发社招面试解答之性能优化,Android开发面试题及答案

android 程序员 移动开发

DeFi平台挖矿系统需求开发(现成案例)

2021年字节跳动74道高级程序员面试,百度Android岗一面+二面内容

android 程序员 移动开发

打破 Serverless 落地边界,阿里云 SAE 发布5大新特性

互联网 科技

Android事件分发机制收藏这一篇就够了,阿里一线架构师技术图谱

android 程序员 移动开发

Android免打包多渠道统计如何实现,技术实现

android 程序员 移动开发

Android小程序开发实例,扔物线五期

android 程序员 移动开发

跨越行业绊脚石,阿里云函数计算发布7大技术突破

阿里巴巴中间件

阿里云 云原生 中间件 函数计算 云栖大会

2021京东Android面试真题,享学课堂android怎么样

android 程序员 移动开发

Android事件分发机制及设计思路,Android程序员校招蚂蚁金服

android 程序员 移动开发

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