博客
关于我
强烈建议你试试无所不能的chatGPT,快点击我
契约式编程
阅读量:2437 次
发布时间:2019-05-10

本文共 1677 字,大约阅读时间需要 5 分钟。

契约是减少大型项目成本的突破性技术。契约由先验条件、后验条件、错误和不变量等概念组成。契约可以而加到 C++ 中而无需对语言加以改造,但是却十分笨拙且不一致。

在语言内部支持契约的目的是:

  1. 给契约一个一致的观感
  2. 提供工具支持
  3. 使编译器能够根据从契约中收集的信息生成更好的代码
  4. 易于管理并强制实行契约
  5. 处理契约继承
Contracts make D bug resistant
 契约的概念很简单——它只是必须为真的表达式。如若不然,契约就被违反,那么按照定义,程序中就一定有 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 契约。

类不变量

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

参考书目


转载地址:http://tjrmb.baihongyu.com/

你可能感兴趣的文章
ts:json串转换成数组
查看>>
String、StringBuffer和StringBuilder的区别
查看>>
java——职责链模式
查看>>
java_选择类排序——简单选择排序
查看>>
java_中介者模式
查看>>
java_备忘录模式
查看>>
多线程——背景了解
查看>>
power designer使Comment与Name相同.txt
查看>>
IE下的图片空隙间距BUG和解决办法
查看>>
[pb]从excel导入数据到datawindow
查看>>
CSS Padding in Outlook 2007 and 2010
查看>>
有关内存的思考题
查看>>
What is the difference between gross sales and revenue?
查看>>
Dreamweaver默认打开后缀名为ftl的文件时
查看>>
LNMP一键安装
查看>>
几个分析函数的比较
查看>>
主流算法:
查看>>
RMI
查看>>
J.U.C之Future
查看>>
缓存思想分析
查看>>