3、契约式设计 Design by Contract
可信软件设计的基础思想
谚语: When ideas fail, words come in very handy !
他人译文“殚思竭虑之时，文字将成为利器” 本人认为“当想法失败时，总会出来许多理由辩解”
3.1 问题的引入 由谁负责系统的可靠性？
3.2 Contract (契约) History
Tony Hoare，把“操作契约 Operation contract”引入了计算机科学的 “形式化规范说明formal specification”研究
In the mid-1960s to develop an ALGOL 60 compiler
Read Bertrand Russell‘s （ 伯特兰·罗素）
Introduction to Mathematical Philosophy, which introduced him to the idea of axiomatic theory（公理）and assertions（断言） 。
Assertions: (pre- and post-conditions)
Peter Lucas, in 1974, VDM(Vienna Definition Method), for PL/1 compiler, at IBM Lab
VDM, A method applied operation contract formal specifications and rigorous proof theory
In the 1980s, Bertrand Meyer, compiler writer
the OO language: Eiffel
started to promote the use of pre- and post-condition assertions as first-class elements within his Eiffel language
契约式设计 Design by Contract (DBC)
细粒度软件类的操作需要强调“契约”，而不是针对整个系统的操作（大粒度软件类）
推动了“不变量 invariant”的概念
在操作执行前、执行后都不变的概念
1990s, Grady Booch
把“契约 contracts”引入对象操作
详细的用例描述中，重要的操作
Pre- / Post- condition
3.3 契约式设计DBC (Design By Contract)
名词解释
客户端、客户 Client：需要另一方提供服务
服务端、服务器 Server：为其它方提供服务
一份契约承载了相互间（client/server) 的义务与利益
客户端只有在能够满足服务端的“前置条件”的情况下，才能调用服务端 的服务
The client should only call a routine（server） when the routine’s pre-condition is respected
服务端在结束服务后，必须保证满足其后置条件
The routine ensures that after completion its post-condition is respected
比喻
顾客到商店买食品。必须是真钱，不是假币。食品必须卫生、安全、符合 质量要求
断言 assertion
在类的代码中，加入一些断言，则定义了契约
Each class defines a contract, by placing assertions inside the code
断言仅仅是一些逻辑表达式 Assertions are just Boolean expressions
断言不影响程序的执行 Assertions have no effect on execution
断言可以被评估，或者忽略 Assertions can be checked or ignored
每个功能定义了一个前置条件、一个后置条件 Each feature is equipped with a precondition and a postcondition
3.4 Software Correctness
假定有一个人拿着一个程序到你面前问: “ 这个程序正确吗？Is this program correct ”
这个问题有意义的前提是: 程序应该完成什么功能有一个精确的描述
This question is meaningful only if there is a precise description of what the program is supposed to do
这样的一个描述，就是规格说明 specification, 规格说明必须精确，否则不可 能推理出是否正确
3.5 规格说明Specification的形式化表示
小结 契约式设计
软件可靠性需要服务的提供方与客户方都有精确的规格说明
Software reliability requires precise specifications which are honoured by both the supplier and the client
契约式设计DbC使用断言（前置条件、后置条件、不变量等）作为 供/需双方之间的契约
uses assertions (pre and postconditions, invariants) as a contract between supplier and client