你在使用哪种编程语言?快来投票,亲手选出你心目中的编程语言之王 了解详情
写点什么

微软新语言 Spec#终结 Null 引用异常

2007 年 4 月 24 日

微软发布了 Spec# 1.0 版本。Spec#是 C#的一个扩展,支持许多契约(contract)属性,如非 Null 类型系统,前置和后置条件,循环常量(loop invariant)和对象常量等。

Null 引用异常(reference exceptions)也许是 C#、Java 和 VB 程序中最普通不过的异常了。为了消除这种错误,Spec#支持一个非 Null 类型系统。在这个系统里,编译器确保用“!”符号标记的变量永不为 Null,比如“Customer! _customer ”。为了便于使用,它允许成员变量在基类构造器(constructors)前就可以被初始化。

非 Null 类型系统还可以扩展到参数、本地变量和返回值。一个例外是数组中的值,因为可能会因数组初始化和 C#的协变数组(covariant array)而导致错误。

前置条件指定对象或者在方法调用前被传递的参数等所需要的状态。比如,开发人员可以通过“requires”语句要求某个集合(collection)为不是只读的,或者要求在 Insert 方法调用前要用到的索引是有效的。不像现在在 C#里面被用到的运行时异常(runtime exception),Spec#希望在编译时就能够设置这些条件。“otherwise”语句可以被用来表示哪些异常会被抛出,如果前置条件不能被静态检查和事后违背的话。

指定了 ensures clause 的后置条件会确保类的常量不被中断,返回的值也在一个可接受的范围。它会先于被调用的方法前存取对象值,所以开发人员也能确保类似数值变量可以一直以 1 为单位增长这样的事情。而且,还被编译器静态地保证。

类似于 Java,Spec#也使用了可检查异常。主要的区别是,在一个发生异常的事件中也许仍可以设置后置条件。这种情况下,开发人员会将 ensures clause 置于 throws clause 之上,以确保所做的修改已经正确回滚。

其中没有提到的地方是 Spec#是如何通过可检查异常(checked exception)处理版本标定(versioning)和继承(inheritance)。在 Java 中,如果说可能会跳出一个基类中没有定义的异常,那么一般很难去通过增加功能性或者子类来扩展类

那些常量很像后置条件(post-condition),但是它们应用到类中所有的方法上。指定了“常量”声明,它们就可以保证在每个方法调用的最后,对象处在一个稳定的条件下。

Spec#严重依赖上面提到的契约类型。但是因为它们不是基础类库(Base Class Library)的一部分,所以 Spec#允许预编译库的契约在一个编译时引用到的分离仓库(repository)中被指定。

查阅英文原文: Spec# Puts an End to Null Reference Exceptions

编辑注:感谢孟岩岳立东对本文部分专业术语的审校。

2007 年 4 月 24 日 00:15396

评论

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

某Javva程序员金秋9月靠这份文档涨薪10K,你把这份Java进阶文档吃透涨薪超简单!

Java成神之路

Java 程序员 架构 面试 编程语言

卧槽,牛皮了!某程序员苦刷这两份算法PDF47天,四面字节斩获心仪大厂offer!

Java成神之路

Java 程序员 架构 面试 编程语言

刷透近200道数据结构与算法,成功加冕“题王”,挤进梦中的字节

Crud的程序员

架构 面试 算法 数据结构与算法

侵犯商业秘密罪律师提醒区块链技术与商业秘密的安全保管

CECBC区块链专委会

时间戳

全面开创城市数字经济新时代

CECBC区块链专委会

数字经济

LeetCode题解:236. 二叉树的最近公共祖先,递归,JavaScript,详细注释

Lee Chen

算法 LeetCode 前端进阶训练营

分布式全链路灰度发布的探索与实践

阿里巴巴云原生

阿里云 微服务 运维 云原生 中间件

腾讯十年,总结出这份Java架构师知识路线,保你稳拿40k+

Java架构追梦

Java 面试 架构师成长笔记 金三银四 全栈知识点

产品风控:短信验证码的风控策略

香芋味的猫丶

短信防刷 产品安全 短信验证码 短信防轰炸 短信防火墙

凭借这份Java超硬核面试 “备战” 手册!我刚面试完字节跳动、阿里、华为、小米等后端岗位

Java架构之路

Java 程序员 架构 面试 编程语言

字节跳动大佬整理的这份《算法中文手册》火了,不少小伙伴靠这份指南成功掌握了算法的核心技能,成功拿到了 BATJ等大厂offer。

Java成神之路

Java 程序员 架构 面试 编程语言

两年Java开发经验,我凭借这份349页的《阿里Java面试通关手册》成功拿到字节跳动Offer。

Java成神之路

Java 程序员 架构 面试 编程语言

化妆品溯源系统开发,区块链防伪溯源

135深圳3055源中瑞8032

没想到,学习带给我最宝贵的东西是底气

Sandy

案例研究之聊聊 QLExpress 源码 (三)

小诚信驿站

刘晓成 小诚信驿站 28天写作 QLExpress源码 聊聊源码

数智化浪潮之中,传统企业如何抓住转型机遇?

京东科技开发者

DevOps

跪了!Alibaba内部出品贼火的Java面试手册,全面对标蚂蚁金服、头条、拼多多等

Java架构之路

Java 程序员 架构 面试 编程语言

智慧社区安防建设的功能,智慧社区建设方案

135深圳3055源中瑞8032

学习,不是一件一蹴而就的事情

Sandy

小马哥刷LeetCode 1480. 一维数组的动态和

小马哥

Java 数据结构与算法 面试数据结构与算法 28天写作

分布式批量任务调度、自动化运维管理监控平台Taskctl

会飞的鱼

kettle 分布式系统 海豚调度 自动化部署 ETL

赫拉利其人其书之我见(2)

石君

28天写作 简史 科技简史

SpringCloud 从入门到精通 05--- 订单模块

Felix

我是如何用几十个小时完成自己的3个flag

Sandy

区块链技术应用新阶段有五大趋势

CECBC区块链专委会

比特币 区块链 数字货币

霸榜各个网站的阿里独有的高并发高并发手册:Netty、Redis、Zookeeper,看完惊呆了!

996小迁

redis zookeeper 架构 面试 Netty

2020年度编程语言排行榜 C语言称霸,Java遭遇滑铁卢?

架构精进之路

编程语言 28天写作

什么是区块链挖矿?区块链怎么挖矿?

v16629866266

波场链DAPP软件APP开发|波场链DAPP系统开发

开發I852946OIIO

系统开发

ArgoCD + KubeVela:以开发者为中心的 GitOps

阿里巴巴云原生

阿里云 开源 容器 云原生 k8s

助力金三银四跳槽季,《Java面试突击版》第四版强势来袭

Java架构之路

Java 程序员 架构 面试 编程语言

围绕“三个问题”开展的网易云音乐数据基础建设

围绕“三个问题”开展的网易云音乐数据基础建设

微软新语言Spec#终结Null引用异常-InfoQ