Design by Contract（契约式设计）

DBC  元素

先验条件:  针对方法（method），它规定了在调用该方法之前必须为真的条件。

后验条件: 也是针对方法，它规定了方法顺利执行完毕之后必须为真的条件。

不变式:  针对整个类，它规定了该类任何实例调用任何方法都必须为真的条件。

DBC 六大原则  

区分命令和查询 

将基本查询同派生查询区分开 

针对每个派生查询，设定一个后验条件，使用一个或多个基本查询的结果来定义它。 

对于每个命令都撰写一个后验条件，规定每个基本查询的值。 

对于每个查询和命令，采用一个合适的先验条件。 

撰写不变式来定义对象的恒定特性 

DBC 六大准则 

在适当的地方添加物理限制。 

先验条件中尽可能使用高效的查询。 

用不变式限定属性。 

为了支持特性的重定义，用相应的先验条件确保每个后验条件。 

将预期发生的变化和框定规则这两种不同的限制分别放置在不同的类中。 

有保密性要求，则违背保密性的查询可以在契约中使用，然后被设为私有属性。

 

Eiffel中的“契约” 

契约关系的双方是平等的，对整个bussiness的顺利进行负有共同责任，没有哪一方可以只享有权利而不承担义务。

契约关系经常是相互的，权利和义务之间往往是互相捆绑在一起的；

执行契约的义务在我，而核查契约的权力在人；

我的义务保障的是你的利益，而你的义务保障的是我的利益； 

我的看法

不管是不变式，还是先验后验条件，都是为了详细定义组件或对象的状态，这是为了防止程序员懒惰造成产品质量下降而强加的框架。

执行起来有难度的是，用户在使用组件的时候，即使知道契约，能否严格按照契约来做，开发期间是否能够将所有的违反契约的地方全部列出来，仍然是一个问题。

所以说是“Design by Contract”，因为详尽的测试还是必不可少的。

在OOA，OOD，OOP中，DBC只是提供了OOD的一种思想，是设计组件接口的一般性的原则

程序设计中的完备性

一个组件的接口构成一个完备的空间，基本查询就是其中的基矢量，派生查询可能很多，但都可以由基矢量的组合来表示。基矢量的所以组合构成这个组件的允许状态空间

命令能够改变组件的状态，使组件从状态空间中的一点迁移到另外一个点

简化接口的复杂性，重要的一点就是减少组件状态空间的大小，可以通过减少基矢量的数目或者减少某个基矢量的取值范围。

精确性和细节  设计阶段要求忽略细节，但也同样丢失了精确性，DbC要求保留模型语义的精确性，避免了设计者和编码人员之间或者使用者和提供者直接的理解误差  契约的应用层次也可以覆盖从设计到编码以至于测试。在设计阶段，了解DbC的人至少不会忽略对违反契约情况的处理，而对这一点缺乏足够的认识是很多产品不够健壮的主因。