标签：其它 pre sid checked ignore with ssi soft 相互
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
标签：其它 pre sid checked ignore with ssi soft 相互
原文地址：https://www.cnblogs.com/mayZhou/p/10548418.html
