1. 规约（specification）、行为等价性

规约是团队合作的关键，也起到了一个契约的作用，代表着程序与客户端之间达成一致。

其次规约给供给双方都确定了责任，在调用时双方都需要遵守。

为什么要写规约：

• 很多bug来自于双方的误解
• 不写下来，不同的开发者的理解可能不同
• 没有规约，难以定位错误

规约的优点：

• 精确地规约，有助于区分责任
• 客户端无需阅读调用方法的代码，只需理解规约即可

行为等价性：

    简单来讲就是客户端视角下，看两个方法是否可以相互替换。站在客户端的角度来讲其不需要知道方法的具体实现过程，其只想知道如何使用方法，方法能做什么？所以规约也就可以判断两个方法是否等价了。若两个方法同时符合同一个规约，这两个方法等价。也变相的说明了规约与实现无关。

2.前置后置条件

契约：当前置条件满足时，后置条件必须满足！如果前置条件不满足，那么开发者（方法）可以做任何事情。

静态类型声明是一种规约，可以据此进行静态类型检查，方法前的注释也是一种规约，但需人工判定是否满足。

mutating方法的规约：

• 除非在后置条件声明过，否则方法内不应该改变输入参数
• 应尽量遵循此规则：尽量不设计mutating的规约，否则容易引起bug
• 程序员之间的默契：除非规约必须如此，否则不应修改输入参数
• 尽量避免使用mutable的对象，mutable对象会让简单的规约边的复杂

3.规约

规约的分类：

• 按规约的确定性
• 按规约的陈述性
• 按规约的强度

强规约与弱规约（Strong specs、weak specs）

如果存在两个规约S1、S2。如果S2的规约强于S1，那么有：

1. S2的前置条件更弱
2. S2的后置条件更强

那么就可以用S2去替代S1。（较强的规约替换较弱的规约）

One栗子：

Two栗子，呸，栗题……

emm……答案已经写在了上面，前置条件更弱后置条件不变，所以应该是变强了。

Tree栗题：

同样规约变强。

Four栗题：

这个就没有办法判断啦，毕竟两个解集合不是包含关系。时刻记住更强的规约代表着更小的解空间！

越强的规约意味着实现者（implementor）的*度与责任越重，而客户（client）的责任越轻。

确定的规约与非确定的规约（Deterministic、Undeterministic specs）

确定的规约（Deterministic specs）：给定一个满足前置条件的输入，，其输出是唯一的明确的。

栗子：

欠定的规约（Under-deterministic specs）：同一个输入可以有多个输出。（通常有确定的实现）

栗子：

未确定的规约（Nondeterministic specs）：同一个输入，多次执行时可能得到的输出结果不同。

操作式规约与声明式规约（Operational specs and Declarative specs）

操作式规约：简单的例子（伪代码）

声明式规约：没有内部实现描述，只有初末状态。

声明式规约相比于上着更有价值，因为内部实现的细节不需要在规约中呈现，应放在内部代码注释中呈现。

栗子：

可见第三个并没有说出内部代码的实现过程，只有一个初末状态，所以应该是第三个为声明式规约。