6.3 契约式设计

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 

上一篇:List JIT 分配策略


下一篇:斜率优化小结