点击围观!腾讯 TAPD 助力金融行业研发提效、敏捷转型最佳实践! 了解详情
写点什么

.NET 4 特性聚焦:代码契约

  • 2008-12-08
  • 本文字数:1240 字

    阅读完需:约 4 分钟

去年,我们已经开始在讨论

Spec#,这是一个基于 C#的支持通过契约来进行设计的语言。以契约来设计是构建于诸如静态类型化这样的概念之上的,特定的动作只有在编译时被验证之后才能执行。契约通常使用前置和后置条件的形式来表示,比如一个参数或返回值永远不能为空或者只能包含某个特定范围的值。

为了不让开发人员学习整个诸如 Spec#这样的新语言,微软正在构建一个独立于语言的函数库,可以被任何.NET 语言所利用。在某些方面,契约 看上去类似断言,不过它们本质上存在非常大的区别。契约通过静态代码分析的组合来实现,它能被用于编译器内部和外部,以及测试框架之中。它们也能被执行, 这意味着它们在运行调试版本的时候和断言很类似。让我们来看第一个例子:

复制代码
string GetDescription(int x){
Contract.Requires(x>0);
Contract.Ensures(Contract.Result<string>() != null);</string>

如果只看签名,开发人员只能获得静态类型的信息“GetDescription 要求输入一个整数并返回一个字符串”。而通过附加契约,开发人员和工具都可以知道“GetDescription 要求输入一个正整数并返回一个不能为空的字符串”。

除了显式的契约之外,契约检查器也支持隐式的契约。一个例子就是被零除这样的情况。如果一个类包含一个整数除法,其中的除数是一个变量,那么所 有的代码路径都必须保证这个变量不会为零或者会引发一个警告。如果在这种情况中的变量是一个开放类的属性,那么它也会要求检查每个子类。对于非关联化空值 和数组索引也存在一些隐式契约。

为了让契约设计更容易,还存在一个 ObjectInvariant 方法的概念。这个特别的方法只包含契约,可以被注入到每个方法调用的末尾以保证对象的状态保持一致。要着重注意的是,这个东西要应用到所有方法之中,包括那些来自于其他程序集的子类。

另外一个节省时间的功能是轻易对旧值的访问。在下面的例子中,Ensures 契约被用于关联 OldValue 语法以确定集合的数目属性是递增的。

复制代码
Public Sub Add(value as Object)
Contract.Ensure(Count = Contract.OldValue(Count) + 1)

虽然契约是写在方法之上的,不过它能被编译器自动地移到 Return 语句之前。由于需要一些系统开销来存储 Count 的旧值,检查器的这种排序操作只在调试编译版本中发生。

为了支持函数库开发人员,发布版本包含了一个引用程序集。例如,Widgets.dll 程序集拥有的大量契约被提取和放置到了程序集 Widgets.Contracts.dll 中。这允许客户端开发人员在利用由函数库开发人员创建的契约时,还是能使用更快的发布编译版本。

一个更有趣的特性是契约不仅仅能应用于实际的函数,甚至没有其他实现细节的接口和抽象方法也能拥有契约。这是通过创建这个接口的一个引用实现来实现,这个引用实现的唯一目的就是持有契约。而这个引用实现则通过特性以连接回接口。

对于契约的内容没有任何限制。由于相同的契约可以用于静态和运行时检查过程,所以,一个不能被评估的约束可能仍然允许被其他的检查。契约也能被文档生成器提取为文档信息。

查看英文原文:.NET 4 Feature Focus: Code Contracts

2008-12-08 04:231709
用户头像

发布了 254 篇内容, 共 49.2 次阅读, 收获喜欢 2 次。

关注

评论

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

一款宝藏工具:Apipost

Xd

Java 后端 接口测试

TiFlash 源码解读(四) | TiFlash DDL 模块设计及实现分析

TiDB 社区干货传送门

集群管理

DDD实战(11):冲刺1代码TDD实现之道

深清秋

DDD 软件架构设计 生鲜电商系统 7月月更

Java基础:集合框架之Collection(List,Set)

百思不得小赵

集合 Java’ 7月月更

2022读过的书--《操作系统导论》

SkyFire

读书 操作系统

电商系统微服务拆分

地下地上

架构师实战营

小程序视图容器

小恺

7月月更

Envoy整体架构概述

阿泽🧸

envoy 7月月更

【刷题记录】6. Z 字形变换

WangNing

7月月更

架构实战营模块 6 作业

星夜

架构实战营

Java注解详情与自定义注解实战

宁在春

aop 注解 反射 Java’ 7月月更

【Docker 那些事儿】如何安全地进入到容器内部

Albert Edison

Docker Kubernetes 容器 云原生 7月月更

2022 读过的书 -- 《Github入门与实践》

SkyFire

GitHub 读书

图解网络:什么是 DNS 域名系统?

wljslmz

网络协议 DNS 网络技术 7月月更 域名系统

批量处理数据神器——Java数组与引用

未见花闻

7月月更

读书笔记之《深入理解Java虚拟机:JVM高级特性与最佳实践》

菜农曰

Java JVM 后端开发 后端技术

拆分电商系统为微服务

Pengfei

动态注册广播流程学习

北洋

Andriod 7月月更

应用容器化迁移步骤

穿过生命散发芬芳

应用迁移 7月月更

有赞们的逻辑变了吗?

科技新知

小程序电商业务微服务设计与基础设施选型

Geek_e8bfe4

kafka 生产者分区策略演进

布兰特

kafka

企业无忧 | Apipost私有化部署活动 火热开启

Xd

后端 接口测试工具

Java中二进制转换的多种方法

秋名山码民

Java’ 7月月更

Python绘制精美可视化数据分析图表(一)-Matplotlib

迷彩

Python 可视化 matplotlib 7月月更

不习惯的Vue3起步二 の alias别名、ref和reactive

空城机

Vue3 7月月更

spring 循环依赖

周杰伦本人

7月月更

leetcode 312. Burst Balloons 戳气球(困难)

okokabcd

LeetCode 动态规划 分治 数据结构与算法

【C 语言】进阶指针 Three

謓泽

7月月更

【LeetCode】装满杯子需要的最短总时长Java题解

Albert

LeetCode 7月月更

大风车吱呀吱哟哟地转,这个风车加载指示组件真有趣!

岛上码农

flutter ios 前端 安卓开发 7月月更

.NET 4特性聚焦:代码契约_.NET_Jonathan Allen_InfoQ精选文章