`
- 浏览:
220979 次
- 性别:
- 来自:
北京
-
契约是减少大型项目成本的突破性技术。契约由先验条件、后验条件、错误和不变量等概念组成。契约可以加到 C++ 中而无需对语言加以改造,但是却十分笨拙且不一致。
在语言内部支持契约的 目的是:
给契约一个一致的观感
提供工具支持
使编译器能够根据从契约中收集的信息生成更好的代码
易于管理并强制实行契约
处理契约继承
契约的概念很简单——它只是必须为真的表达式。如若不然,契约就被违反,那么按照定
义,程序中就一定有 bug 。
契约构成了程序规格说明的一部分,只不过是从文档中挪到了代码中。就像每个程序员所知道的那样,文档通常是不完整的、过时的、错误的或者是不存在的。
将契约挪到代码中就使得契约变得可对程序验证了。
断言契约
最基本的契约是断言。 断言在代码内插入一个可检查的表达式,这个表达式在正常情况下
必须为真:
assert(expression);
C 程序员会有似曾相识的感觉。但是与 C 不同的是,函数体内的 assert 会抛出
AssertException ,这个异常可以被捕获并处理。如果代码必须处理其他代码对其的误用,
如果代码必须是失败可证的,捕获契约违规就很有用,它同样也是调试的有力工具。
契约先验条件和契约后验条件契约先验条件指出语句执行的先验条件条件。
最典型的用法可能要数验证函数参数的有效性了。契约后验条件验证语句的结果。最典型的用法要数验证函数返回值得合法性以及它的任何副作用。
语法结构为:
in
{
...契约先验条件...
}
out (result)
{
...契约后验条件...
}
body
{
...代码...
}
按照定义,如果契约先验条件被违反,则过程体(body)将受到错误的参数。这将抛出一个
InException 异常。如果契约后验条件被违反,则意味着过程体中有一个 bug ,将抛出一个 OutException 异常。
in 或 out 子句都可以被省略。如果过程体带有有 out 子句 ,变量 result 将被声明并被赋给函数的返回值。例如,我们实现一个求平方根的函数:
long square_root(long x)
in
{
assert(x >= 0);
}
out (result)
{
assert((result * result) == x);
}
body
{
return math.sqrt(x);
}
in 和 out 中的断言叫做 契约。其中可以出现任何 D 的语句或者表达式,但是必须要保证这些语句没有副作用,并且最终发行版中的代码不依赖于这些代码的作用。在构建发行版的程
序时,这些代码将不会包括在其中。
如果函数返回 void,即没有结果,那么 out 字句中自然也没有 result 的声明。在这种情况下,使用:
void func()
out
{
...契约...
}
body
{
...
}
在 out 语句中,result 被初始化并设为函数的返回值。
编译器可以设计为每个 in 和 inout 参数都在 in { } 中被引用,并且每个 out 和 inout 参数都在 out { } 中被引用。
in-out 语句也可以被用在函数内部,例如,可以用来检查循环的结果:
in
{
assert(j == 0);
}
out
{
assert(j == 10);
}
body
{
for (i = 0; i < 10; i++)
j++;
}
这个特性目前尚未实现。
In,Out和继承
如果派生类的函数重写了父类中的一个函数,那么它只须满足基类函数的一条 in 契约。重
写函数 放松 了契约。
反过来,所有的 out 契约都必须满足,所以重写函数 收紧 了 out 契约。
类不变量
类的不变量用来指定类中总是为真(除了在执行成员函数时)的特性。它们在 类 中介绍。.
。。。。
分享到:
Global site tag (gtag.js) - Google Analytics
相关推荐
在本文中,我们将深入探讨数字微镜器件(Digital Micromirror Device,简称DMD)的编程,特别是关于DMD时间积分、帧频设置以及画面大小调整等关键参数的设定。DMD是投影系统中的一种核心组件,常用于德州仪器(Texas...
动态模态分解(Dynamic Mode Decomposition,简称DMD)是一种数据驱动的方法,广泛应用于流体动力学、信号处理和工程领域,用于分析复杂系统的行为。在这个“DMD.zip”压缩包中,包含的是一个关于DMD应用的具体实例...
【Dmd编译器学习笔记】是一份详细探讨Dmd编译器的资源集合,它涵盖了如何理解和使用这个强大的D语言编译工具。D语言是一种高效、现代化的系统编程语言,设计时兼顾了性能和可读性。Dmd作为D语言的官方编译器,对于...
动态模态分解(Dynamic Mode Decomposition,简称DMD)是一种数据驱动的分析方法,主要用于处理时间序列数据,特别是在流体动力学、机械工程和信号处理等领域广泛应用。它能揭示复杂系统内部的动力学行为,通过将...
【DMD2-master_DMD_】是一个与动态模式分解(DMD, Dynamic Mode Decomposition)相关的源代码库。DMD是一种强大的数据分析技术,主要用于处理时间序列数据,特别是应用于流体动力学、信号处理和图像分析等领域。这个...
数字微镜装置DMD是由美国德州仪器公司(Texas Instruments,简称TI)于1987年发明的一种利用半导体制造技术的高速数字式光反射开关阵列器件。DMD的核心部件是微镜,微镜片围绕一个固定的轴(轭)旋转,通过改变微...
动态模式分解的matlab 代码,有注释
通过阅读和理解DMD的源代码,开发者可以学习到编译原理的实际应用,了解语言特性的底层实现,这对于提升编程技能和解决实际问题大有裨益。 在这个特定的版本dmd.2.026中,可能会包含一些新的特性、优化或者bug修复...
在本资源"POD_DMD-master.zip"中,包含的是一套针对CFD数据进行处理和分析的方法,主要涉及两种关键的技术:主成分分析(PCA,Principal Component Analysis)也称为POD( Proper Orthogonal Decomposition)和动态...
乐创自动化生产的DMD403及DMD403A步进电机驱动器是一款高性能、价格低廉的产品,适合于驱动两相或四相的混合式步进电机。该驱动器采用了双极性恒流斩波技术,能较其他驱动方式输出更大的功率。同时,它还具有细分...
DMD402及DMD402A-B使用手册pdf,DMD402及DMD402A-B使用手册
### 一、DMD15/DMD15L卫星调制解调器概述 **标题**: DMD15/DMD15L **描述**: 该设备为一种卫星调制解调器(Satellite Modem),型号为DMD15/DMD15L,适用于IBS/IDR通用系统。它提供了安装与操作手册(Installation...
根据提供的文档信息,我们可以提取出以下有关DMD(Digital Micromirror Device)板的相关知识点,主要用于DLP(Digital Light Processing)技术,该技术是由TI(德州仪器)公司开发的。 首先,DMD板是DLP系统中的...
2. **灵活可编程性**:FPGA的灵活性使得系统能够快速适应不同的应用场景,比如通过软件重新配置来满足特定的应用需求。 3. **压缩感知**:在压缩感知领域,FPGA可以实现高效的算法加速,减少数据处理延迟,提升整体...
标题中的“PODandDMD”指的是两种在流体力学和信号处理领域广泛使用的数据分析方法:本征正交分解( Proper Orthogonal Decomposition,简称POD)和动态模态分解(Dynamic Mode Decomposition,简称DMD)。...
标题中的“dmd.rar_DMD”很可能指的是“Dot Matrix Display”(点阵显示器)的库文件,用于在Arduino平台上操作矩阵显示屏。这个压缩包可能包含了实现这种显示效果所需的代码和其他资源。 Arduino DMD库是专门为在...
在IT领域,刷机通常指的是对电子设备,如智能手机、电视盒或数字卫星接收器(如DMD500)的操作系统进行更新或替换的过程。本文将详细讲解DMD500的串口刷机教程,包括串口备份与恢复等关键步骤。 首先,了解DMD500。...
8. 系统控制功能包括I2C设备配置控制、最多3个LED的可编程电流控制、集成的DMD重置驱动控制以及DMD水平和垂直显示图像。 9. 低功耗设计,典型情况下只有93mW的翻转功耗。 10. 支持外部内存,包括166-MHz的移动DDR ...
《DFL for DMD2.031:深入解析D语言源码与工具的整合应用》 DFL,全称为D Foundation Library,是为D语言(D Programming Language)设计的一个强大的开源库,它旨在提供一系列实用的、高效的、易于使用的模块,以...