`
hqs7636
  • 浏览: 220975 次
  • 性别: Icon_minigender_1
  • 来自: 北京
社区版块
存档分类
最新评论

契约式编程(dmd 1.00)

阅读更多
契约是减少大型项目成本的突破性技术。契约由先验条件、后验条件、错误和不变量等概念组成。契约可以加到 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 契约。


类不变量

类的不变量用来指定类中总是为真(除了在执行成员函数时)的特性。它们在 类 中介绍。.





。。。。
分享到:
评论

相关推荐

    DMD.zip_DMD_DMD时间积分_dmd 编程_dmd编程

    在本文中,我们将深入探讨数字微镜器件(Digital Micromirror Device,简称DMD)的编程,特别是关于DMD时间积分、帧频设置以及画面大小调整等关键参数的设定。DMD是投影系统中的一种核心组件,常用于德州仪器(Texas...

    DMD.zip_DMD_DMD模态_dmd特征值_selectps3_动态模态分解

    动态模态分解(Dynamic Mode Decomposition,简称DMD)是一种数据驱动的方法,广泛应用于流体动力学、信号处理和工程领域,用于分析复杂系统的行为。在这个“DMD.zip”压缩包中,包含的是一个关于DMD应用的具体实例...

    Dmd编译器学习笔记

    【Dmd编译器学习笔记】是一份详细探讨Dmd编译器的资源集合,它涵盖了如何理解和使用这个强大的D语言编译工具。D语言是一种高效、现代化的系统编程语言,设计时兼顾了性能和可读性。Dmd作为D语言的官方编译器,对于...

    DMD-code_matlab_DMD_

    动态模态分解(Dynamic Mode Decomposition,简称DMD)是一种数据驱动的分析方法,主要用于处理时间序列数据,特别是在流体动力学、机械工程和信号处理等领域广泛应用。它能揭示复杂系统内部的动力学行为,通过将...

    DMD2-master_DMD_

    【DMD2-master_DMD_】是一个与动态模式分解(DMD, Dynamic Mode Decomposition)相关的源代码库。DMD是一种强大的数据分析技术,主要用于处理时间序列数据,特别是应用于流体动力学、信号处理和图像分析等领域。这个...

    基于FPGA的DMD驱动控制电路的研究设计.pdf

    数字微镜装置DMD是由美国德州仪器公司(Texas Instruments,简称TI)于1987年发明的一种利用半导体制造技术的高速数字式光反射开关阵列器件。DMD的核心部件是微镜,微镜片围绕一个固定的轴(轭)旋转,通过改变微...

    DMD.rar_DMD 代码_dmd matlab程序_dmd分解_matlab dmd_分解

    动态模式分解的matlab 代码,有注释

    编译器源代码之:DMD(D语言)dmd.2.026

    通过阅读和理解DMD的源代码,开发者可以学习到编译原理的实际应用,了解语言特性的底层实现,这对于提升编程技能和解决实际问题大有裨益。 在这个特定的版本dmd.2.026中,可能会包含一些新的特性、优化或者bug修复...

    POD_DMD-master.zip_CFD_DMD_POD_模态分析_降阶

    在本资源"POD_DMD-master.zip"中,包含的是一套针对CFD数据进行处理和分析的方法,主要涉及两种关键的技术:主成分分析(PCA,Principal Component Analysis)也称为POD( Proper Orthogonal Decomposition)和动态...

    乐创自动化 DMD403及DMD403A步进电机细分驱动器使用手册.pdf

    乐创自动化生产的DMD403及DMD403A步进电机驱动器是一款高性能、价格低廉的产品,适合于驱动两相或四相的混合式步进电机。该驱动器采用了双极性恒流斩波技术,能较其他驱动方式输出更大的功率。同时,它还具有细分...

    DMD402及DMD402A-B使用手册.pdf

    DMD402及DMD402A-B使用手册pdf,DMD402及DMD402A-B使用手册

    DMD15/DMD15L

    ### 一、DMD15/DMD15L卫星调制解调器概述 **标题**: DMD15/DMD15L **描述**: 该设备为一种卫星调制解调器(Satellite Modem),型号为DMD15/DMD15L,适用于IBS/IDR通用系统。它提供了安装与操作手册(Installation...

    Schematic-FLD3 DMD Board.pdf

    根据提供的文档信息,我们可以提取出以下有关DMD(Digital Micromirror Device)板的相关知识点,主要用于DLP(Digital Light Processing)技术,该技术是由TI(德州仪器)公司开发的。 首先,DMD板是DLP系统中的...

    DMD驱动板设计/FPGA

    2. **灵活可编程性**:FPGA的灵活性使得系统能够快速适应不同的应用场景,比如通过软件重新配置来满足特定的应用需求。 3. **压缩感知**:在压缩感知领域,FPGA可以实现高效的算法加速,减少数据处理延迟,提升整体...

    PODandDMD_本征正交分解_动模态分解_POD和DMD_

    标题中的“PODandDMD”指的是两种在流体力学和信号处理领域广泛使用的数据分析方法:本征正交分解( Proper Orthogonal Decomposition,简称POD)和动态模态分解(Dynamic Mode Decomposition,简称DMD)。...

    dmd.rar_DMD

    标题中的“dmd.rar_DMD”很可能指的是“Dot Matrix Display”(点阵显示器)的库文件,用于在Arduino平台上操作矩阵显示屏。这个压缩包可能包含了实现这种显示效果所需的代码和其他资源。 Arduino DMD库是专门为在...

    DMD500刷机教程

    在IT领域,刷机通常指的是对电子设备,如智能手机、电视盒或数字卫星接收器(如DMD500)的操作系统进行更新或替换的过程。本文将详细讲解DMD500的串口刷机教程,包括串口备份与恢复等关键步骤。 首先,了解DMD500。...

    digital controller for the dlp3000 dmd

    8. 系统控制功能包括I2C设备配置控制、最多3个LED的可编程电流控制、集成的DMD重置驱动控制以及DMD水平和垂直显示图像。 9. 低功耗设计,典型情况下只有93mW的翻转功耗。 10. 支持外部内存,包括166-MHz的移动DDR ...

    DFL for DMD2.031

    《DFL for DMD2.031:深入解析D语言源码与工具的整合应用》 DFL,全称为D Foundation Library,是为D语言(D Programming Language)设计的一个强大的开源库,它旨在提供一系列实用的、高效的、易于使用的模块,以...

Global site tag (gtag.js) - Google Analytics