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