作者：HW-HM
最近陆陆续续讲了几次《代码健壮之道》软件工程精品培训，有一些心得体会，在此写出来供其他讲师和学员参考。
一、软件健壮之道
健壮性 = 健壮的软件 + 安全的部署
健壮的软件 = 外部防御 + 内部正确
在系统边界防御非法输入和安全攻击，构造出一道栅栏，使得系统内部的数据都是合法的，保证健壮性；在系统内部按照契约协作，并采取一些防错和主动暴露错误的手段，保证正确性。
二、契约式设计
1. 契约式设计的定义：明确定义软件模块的权力和义务，并通过程序来检查，以确保程序正确性。
2. 为什么需要契约：契约可以保障双方的利益，降低协作成本。契约合同明确地规定了双方的权力和义务，对于甲方（客户），合同规定了乙方（供应者）要做的工作；对于乙方，合同说明了如果约定的条件不满足，乙方没有义务一定要完成规定的任务。契约规定了准入、准出条件，以及双方的配合事宜，保障各方利益的同时，也降低了协作成本。
3. 契约适用范围：双方可信任。最好的朋友要借钱，一个电话就搞定；熟人借钱，打个欠条即可；陌生人要协作，往往得签署有法律效应的正式合同。这些都是契约的表现形式，铁哥们我本来就信任他，所以直接借钱给他，签正式合同其实也是在两个陌生人之间建立信任。所以归根结底我们可以说，双方可信任，则可按契约协作。对于软件来说，系统外部是不可信的，譬如用户输入、网络数据等，这些数据有可能就是黑客构造的，因此不能按契约协作，对这些不能做任何假定（信任），要进行严格的检查，也就是要在系统边界重点防御。系统内部的数据是可信的，可以按照契约来协作。
4. 如何保障按契约协作：检查契约，违背惩罚。在现实中，一个好友借了我的钱没还我，我就会和他割袍断义，并和那些认识他的人讲，“那小子无情无义，毫无信用，借了我的钱，说好一年还的，现在花儿都谢了三次了，还没还”，结果他声名狼籍，谁也不愿意再借钱给他，这就是对他的惩罚，当然，他也失去了我这个朋友。软件中也类似，我们使用断言来检查契约，如果断言失败（契约被违背了），程序就终止运行，这就是对违背契约的惩罚。通常对这些条件的检查都由实现者完成。
5. 违背契约意味着什么：程序Bug。契约有三类：
先验条件：进入一段代码（函数）之前必须满足的条件，这是调用者的义务，实现者的权力。如果不满足，说明调用者有缺陷。
后验条件：退出一段代码（函数）之后必须满足的条件，这是实现者的义务，调用者的权力。如果不满足，说明实现者有缺陷。
不变条件：在进入之前满足，在退出之后也要满足的条件，通常针对一个类。这是双方的权力和义务。如果不满足，说明程序有缺陷。
对这些契约的违背意味着程序Bug。但有一种例外，就是输入都是OK的，可是我因为一些客观原因（譬如系统资源不足）还是没有搞定任务，这时我需要告诉调用者出了错，对这种情况我们建议使用异常。真正的异常是对方完全满足了契约，而我方仍然没有如约完成任务。
6. 契约式设计六大原则：六大原则的应用是一个设计过程。
区分命令和查询。查询返回一个结果，但不改变对象的可见性质。命令改变对象的状态，但不返回结果（应当是不一定返回结果）。
将基本查询同派生查询分开。派生查询可以用基本查询来定义。
针对每个派生查询，设定一个后验条件，使用一个或多个基本查询的结果来定义它。这样我们只要知道基本查询的值，也就能知道派生查询的值。
对于每个命令都撰写一个后验条件，规定每个基本查询的值。结合“用基本查询定义派生查询”的原则，我们现在已经能够知道每个命令的全部可视效果。
对于每个查询和命令，采用一个合适的先验条件。先验条件限定了客户调用查询和命令的时机。
撰写不变式来定义对象的恒定特性。类是某种抽象的体现，应当将注意力集中在最重要的属性上，以帮助读者建立关于类抽象的正确概念模型。
以学生排队买票的例子说明。先分析业务场景识别出需要的公共函数：
a) 学生到队尾排队（EnQueue，命令）。
b) 学生买完票出队（DeQueue，命令）。
c) 售票员叫下一个学生买票（Head，查询）。
d) 票售完或者售票员下班，队列解散（Clear，查询）。
然后分析这些函数的先验条件、后验条件，以DeQueue说明：
a) 先验条件：队列不空。需要有检查队列长度的查询size。
b) 后验条件：队列长度减一；如果队列不空，则现在的队首，是出队前队首的下一个。第一个条件，需要查询size，已有了。第二个，需要获取某个位置的元素的查询ElementAt(n)。
对所有的公共函数分析完之后，我们可以得出所有的命令和查询，然后我们选取一种方式（例如数组、链表）实现，得出不变式。我们最后才考虑实现，只有少数的函数依赖于我们选择的实现方式，同时所有的命令都可以通过查询来检验，设计灵活，而且易验证，这就是契约式设计的好处。再加上我们对先验条件的检查，也方便发现调用者的缺陷。
7. 断言VS测试：用测试验证外部功能，用断言验证内部实现。测试只能通过构造输入，验证输出，无法验证内部实现。可用断言对函数的局部性结果进行验证，譬如在循环结束时，使用断言检查循环结束条件是否正确。另外在对一个函数进行优化时，可以将原函数保留，并使用它来验证新函数的正确性。
契约式设计部分就总结这么多了，欢迎大家讨论。
苏公安网备 32011402010933号