fbpx
维基百科

契约式设计

契约式设计(英語:Design by Contract,縮寫為 DbC),一种设计计算机软件的方法。这种方法要求软件设计者为软件组件定义正式的,精确的并且可验证的接口,这样,为传统的抽象数据类型又增加了先验条件、后验条件和不变式。这种方法的名字里用到的“契约”或者说“契约”是一种比喻,因为它和商业契约的情况有点类似。

契约式设计模式

因为“Design by Contract”是属于Eiffel Software的注册商标,很多开发人员用契約式編程(Programming by Contract),契約編程(Contract Programming),或者契約優先式開發(Contract-First development)来指代这种方法。微軟也採用這種設計方法,稱為程式碼合約(Code Contracts)。

歷史 编辑

這個術語最早由伯特蘭·邁耶於1986年提出。他設計了Eiffel程式語言來實現這種程式設計方法,在《物件導向軟體建構》(Object-Oriented Software Construction)一書中,又提出兩個後繼版本。2003年,由伯特蘭·邁耶創建的Eiffel software公司,申請將“Design by Contract”作為商標,於2004年通過。

契约式设计應用了形式验证形式规定英语Formal specification霍尔逻辑的理論。

描述 编辑

DbC的核心思想是对软件系统中的元素之间相互合作以及“责任”与“权利”的比喻。这种比喻从商业活动中“客户”与“供应商”达成“契约”而得来。例如:

  • 供应商必须提供某种产品(责任),并且他有权期望客户已经付款(权利)。
  • 客户必须付款(责任),并且有权得到产品(权利)。
  • 契约双方必须履行那些对所有契约都有效的责任,如法律和规定等。

同样的,如果在面向对象程序设计中一个的函数提供了某种功能,那么它要:

  • 期望所有调用它的客户模块都保证一定的进入条件:这就是函数的先验条件—客户的义务和供应商的权利,这样它就不用去处理不满足先验条件的情况。
  • 保证退出时给出特定的属性:这就是函数的后验条件英语Postcondition—供应商的义务,显然也是客户的权利。
  • 在进入时假定,并在退出时保持一些特定的属性:不变条件

契约就是这些权利和义务的正式形式。我们可以用“三个问题”来总结DbC,并且作为设计者要经常问:

  • 它期望的是什么?
  • 它要保证的是什么?
  • 它要保持的是什么?

很多程式語言都有对这种断言的支持。然而DbC认为这些契约对于软件的正确性至关重要,它们应当是设计过程的一部分。实际上,DbC提倡首先写断言。

契约的概念扩展到了方法/过程的级别。对于一个方法的契约通常包含下面这些信息:

  • 可接受和不可接受的值或类型,以及它们的含义
  • 返回的值或类型,以及它们的含义
  • 可能出现的错误以及异常情况的值和类型,以及它们的含义
  • 副作用
  • 先验条件
  • 后验条件英语Postcondition
  • 不变条件
  • (不太常见)性能上的保证,如所用的时间和空间

继承中的子类型可以弱化先验条件(但不可以加强它们),并且可以加强后验条件和不变式(但不能弱化它们)。这些原则很接近Liskov代換原則

所有类之间的关系就是客户与供应商的关系。一个客户在调用供应商的功能时有义务不去违反供应商所需的状态。相应的,供应商也有义务为客户提供它所需的状态和数据。例如,供应商的delete功能要求客户在data buffer当中有数据存在。相应的,供应商要保证当delete功能完成后,data buffer中的数据已被删除。其它的设计契约还有不变式。不变式保证类的状态在任何功能被执行后都保持在一个可接受的状态。

当使用契约时,供应商不应对契约条件是否被满足进行校验。大体的思想是,利用契约条件校验为保护网,在契约被违反的情况下代码会“硬性失败”(fail hard)。DbC的“硬性失败”概念让对契约行为的调试变简单,因为每个过程的行为意图被定义得很清楚。它和一种叫作防御性编程的方法明顯不同,在那种方法里,供应商要负责解决先验条件不满足的情况。相对通常的情况下,在DbC和防御性编程中,如果客户违反了先验条件供应商都会抛出异常—由客户来负责解决这种情况。DbC让供应商的工作更简单。

DbC同时也定义了软件模块的正确性条件:

  • 如果对一个供应商的调用之前类的不变式和先验条件是真,那么在调用后不变式和后验条件也为真。
  • 当调用供应商时,软件模块应保证不违反供应商的先验条件。

因为契约条件在程序运行中不应被违反,它们可以只作为调试代码,或者在发布版本中被移除从而得到更好的性能。

DbC也能帮助代码重用,因为每段代码的契约都被很好的文档化了。模块的契约可以被当做软件文档来描述模块的行为。

语言支持 编辑

原生支持语言 编辑

贯彻契约式设计特征最多的语言包含:

  • Ada 2012
  • Ciao英语Ciao (programming language)
  • Clojure
  • Cobra英语Cobra (programming language)
  • D[1]
  • Dafny英语Dafny
  • Eiffel
  • Fortress英语Fortress (programming language)
  • Kotlin
  • Mercury
  • Oxygene英语Oxygene (programming language)(曾叫做Chrome和Delphi Prism[2]
  • Racket[3]
  • Sather英语Sather
  • Scala[4][5]
  • SPARK(经过Ada程序的静态分析
  • Vala
  • VDM英语Vienna Development Method

通过第三方支持的语言 编辑

  • Ada,通过GNAT的先决条件和后置条件的pragma。
  • CC++:
    • Boost.Contract (页面存档备份,存于互联网档案馆
    • DBC for C预处理器
    • GNU Nana
    • eCv和eCv++ 形式验证工具
    • Digital Mars英语Digital Mars C++编译器,通过C的CTESK扩展。
    • Loki库,提供叫做ContractChecker的机制用来验证一个类服从契约设计。
    • DBC C++[6]
  • C#(和其他.NET语言),通过Code Contracts[7]
  • Groovy,通过GContracts。
  • Go,通过dbc[8]或gocontracts[9]
  • Java:
    • OValOVal,经由AspectJ英语AspectJ
    • Contracts for Java[10](Cofoja)
    • Java建模语言英语Java Modeling Language(JML)
    • Bean Validation英语Bean Validation(只有先决条件和后置条件)[11]
    • valid4j (页面存档备份,存于互联网档案馆
  • JavaScript,通过AspectJS(特别是AJS_Validator)、Cerny.js、ecmaDebug、jsContract、dbc-code-contracts[12]或jscategory。
  • Common Lisp,通过宏设施或CLOS元对象协议
  • Nemerle,通过宏。
  • Nim,通过宏[13]
  • Perl,通过CPAN模块Class::Contract(出自Damian Conway英语Damian Conway)或Carp::Datum(出自Raphael Manfredi)。
  • PHP,通过PhpDeal[14]Praspel英语Praspel或Stuart Herbert的ContractLib。
  • Python,使用包如deal[15]、icontract、PyContracts、Decontractors、dpcontracts、zope.interface、PyDBC或Contracts for Python。
  • Ruby,通过Brian McCallister的DesignByContract、Ruby DBC ruby-contract或contracts.ruby。
  • Rust,通过contracts[16] crate。
  • Tcl,通过XOTcl英语XOTcl面向对象扩展。

参考文献 编辑

  1. ^ Bright, Walter. . Digital Mars. 2014-11-01 [2014-11-10]. (原始内容存档于2014-11-28). 
  2. ^ Hodges, Nick. . Embarcadero Technologies. [20 January 2016]. (原始内容存档于2021-04-26). 
  3. ^ Findler, Felleisen Contracts for Higher-Order Functions (页面存档备份,存于互联网档案馆
  4. ^ . EPFL. [2019-05-24]. (原始内容存档于2019-12-25). 
  5. ^ Strong typing as another "contract enforcing" in Scala, see discussion at scala-lang.org/ (页面存档备份,存于互联网档案馆).
  6. ^ DBC C++ (页面存档备份,存于互联网档案馆) Design by contract for C++
  7. ^ . msdn.microsoft.com. [2022-03-02]. (原始内容存档于2022-06-04). 
  8. ^ . [2022-03-02]. (原始内容存档于2022-06-04). 
  9. ^ . [2022-03-02]. (原始内容存档于2022-06-03). 
  10. ^ . [2022-03-02]. (原始内容存档于2022-03-03). 
  11. ^ . beanvalidation.org. [2022-03-02]. (原始内容存档于2014-07-16). 
  12. ^ . [2022-03-02]. (原始内容存档于2021-11-04). 
  13. ^ . [2022-03-02]. (原始内容存档于2022-06-06). 
  14. ^ . [2022-03-02]. (原始内容存档于2022-06-04). 
  15. ^ . [2022-03-02]. (原始内容存档于2022-06-13). 
  16. ^ . [2022-03-02]. (原始内容存档于2022-05-31). 

外部链接 编辑

  • The Power of Design by Contract(TM) (页面存档备份,存于互联网档案馆) A top-level description of DbC, with links to additional resources.
  • Building bug-free O-O software: An introduction to Design by Contract(TM) (页面存档备份,存于互联网档案馆) Older material on DbC.
  • Benefits and drawbacks; implementation in RPS-Obix Archive.is的存檔,存档日期2013-02-01
  • Bertrand Meyer, Applying "Design by Contract" (页面存档备份,存于互联网档案馆), IEEE Computer, October 1992.
  • Using Code Contracts for Safer Code (页面存档备份,存于互联网档案馆

契约式设计, 英語, design, contract, 縮寫為, 一种设计计算机软件的方法, 这种方法要求软件设计者为软件组件定义正式的, 精确的并且可验证的接口, 这样, 为传统的抽象数据类型又增加了先验条件, 后验条件和不变式, 这种方法的名字里用到的, 契约, 或者说, 契约, 是一种比喻, 因为它和商业契约的情况有点类似, 模式因为, design, contract, 是属于eiffel, software的注册商标, 很多开发人员用契約式編程, programming, contract, 契約編程,. 契约式设计 英語 Design by Contract 縮寫為 DbC 一种设计计算机软件的方法 这种方法要求软件设计者为软件组件定义正式的 精确的并且可验证的接口 这样 为传统的抽象数据类型又增加了先验条件 后验条件和不变式 这种方法的名字里用到的 契约 或者说 契约 是一种比喻 因为它和商业契约的情况有点类似 契约式设计模式因为 Design by Contract 是属于Eiffel Software的注册商标 很多开发人员用契約式編程 Programming by Contract 契約編程 Contract Programming 或者契約優先式開發 Contract First development 来指代这种方法 微軟也採用這種設計方法 稱為程式碼合約 Code Contracts 目录 1 歷史 2 描述 3 语言支持 3 1 原生支持语言 3 2 通过第三方支持的语言 4 参考文献 5 外部链接歷史 编辑這個術語最早由伯特蘭 邁耶於1986年提出 他設計了Eiffel程式語言來實現這種程式設計方法 在 物件導向軟體建構 Object Oriented Software Construction 一書中 又提出兩個後繼版本 2003年 由伯特蘭 邁耶創建的Eiffel software公司 申請將 Design by Contract 作為商標 於2004年通過 契约式设计應用了形式验证 形式规定 英语 Formal specification 與霍尔逻辑的理論 描述 编辑DbC的核心思想是对软件系统中的元素之间相互合作以及 责任 与 权利 的比喻 这种比喻从商业活动中 客户 与 供应商 达成 契约 而得来 例如 供应商必须提供某种产品 责任 并且他有权期望客户已经付款 权利 客户必须付款 责任 并且有权得到产品 权利 契约双方必须履行那些对所有契约都有效的责任 如法律和规定等 同样的 如果在面向对象程序设计中一个类的函数提供了某种功能 那么它要 期望所有调用它的客户模块都保证一定的进入条件 这就是函数的先验条件 客户的义务和供应商的权利 这样它就不用去处理不满足先验条件的情况 保证退出时给出特定的属性 这就是函数的后验条件 英语 Postcondition 供应商的义务 显然也是客户的权利 在进入时假定 并在退出时保持一些特定的属性 不变条件 契约就是这些权利和义务的正式形式 我们可以用 三个问题 来总结DbC 并且作为设计者要经常问 它期望的是什么 它要保证的是什么 它要保持的是什么 很多程式語言都有对这种断言的支持 然而DbC认为这些契约对于软件的正确性至关重要 它们应当是设计过程的一部分 实际上 DbC提倡首先写断言 契约的概念扩展到了方法 过程的级别 对于一个方法的契约通常包含下面这些信息 可接受和不可接受的值或类型 以及它们的含义 返回的值或类型 以及它们的含义 可能出现的错误以及异常情况的值和类型 以及它们的含义 副作用 先验条件 后验条件 英语 Postcondition 不变条件 不太常见 性能上的保证 如所用的时间和空间继承中的子类型可以弱化先验条件 但不可以加强它们 并且可以加强后验条件和不变式 但不能弱化它们 这些原则很接近Liskov代換原則 所有类之间的关系就是客户与供应商的关系 一个客户在调用供应商的功能时有义务不去违反供应商所需的状态 相应的 供应商也有义务为客户提供它所需的状态和数据 例如 供应商的delete功能要求客户在data buffer当中有数据存在 相应的 供应商要保证当delete功能完成后 data buffer中的数据已被删除 其它的设计契约还有不变式 不变式保证类的状态在任何功能被执行后都保持在一个可接受的状态 当使用契约时 供应商不应对契约条件是否被满足进行校验 大体的思想是 利用契约条件校验为保护网 在契约被违反的情况下代码会 硬性失败 fail hard DbC的 硬性失败 概念让对契约行为的调试变简单 因为每个过程的行为意图被定义得很清楚 它和一种叫作防御性编程的方法明顯不同 在那种方法里 供应商要负责解决先验条件不满足的情况 相对通常的情况下 在DbC和防御性编程中 如果客户违反了先验条件供应商都会抛出异常 由客户来负责解决这种情况 DbC让供应商的工作更简单 DbC同时也定义了软件模块的正确性条件 如果对一个供应商的调用之前类的不变式和先验条件是真 那么在调用后不变式和后验条件也为真 当调用供应商时 软件模块应保证不违反供应商的先验条件 因为契约条件在程序运行中不应被违反 它们可以只作为调试代码 或者在发布版本中被移除从而得到更好的性能 DbC也能帮助代码重用 因为每段代码的契约都被很好的文档化了 模块的契约可以被当做软件文档来描述模块的行为 语言支持 编辑原生支持语言 编辑 贯彻契约式设计特征最多的语言包含 Ada 2012 Ciao 英语 Ciao programming language Clojure Cobra 英语 Cobra programming language D 1 Dafny 英语 Dafny Eiffel Fortress 英语 Fortress programming language Kotlin Mercury Oxygene 英语 Oxygene programming language 曾叫做Chrome和Delphi Prism 2 Racket 3 Sather 英语 Sather Scala 4 5 SPARK 经过Ada程序的静态分析 Vala VDM 英语 Vienna Development Method 通过第三方支持的语言 编辑 Ada 通过GNAT的先决条件和后置条件的pragma C和C Boost Contract 页面存档备份 存于互联网档案馆 DBC for C预处理器 GNU Nana eCv和eCv 形式验证工具 Digital Mars 英语 Digital Mars C 编译器 通过C的CTESK扩展 Loki库 提供叫做ContractChecker的机制用来验证一个类服从契约设计 DBC C 6 C 和其他 NET语言 通过Code Contracts 7 Groovy 通过GContracts Go 通过dbc 8 或gocontracts 9 Java OValOVal 经由AspectJ 英语 AspectJ Contracts for Java 10 Cofoja Java建模语言 英语 Java Modeling Language JML Bean Validation 英语 Bean Validation 只有先决条件和后置条件 11 valid4j 页面存档备份 存于互联网档案馆 JavaScript 通过AspectJS 特别是AJS Validator Cerny js ecmaDebug jsContract dbc code contracts 12 或jscategory Common Lisp 通过宏设施或CLOS元对象协议 Nemerle 通过宏 Nim 通过宏 13 Perl 通过CPAN模块Class Contract 出自Damian Conway 英语 Damian Conway 或Carp Datum 出自Raphael Manfredi PHP 通过PhpDeal 14 Praspel 英语 Praspel 或Stuart Herbert的ContractLib Python 使用包如deal 15 icontract PyContracts Decontractors dpcontracts zope interface PyDBC或Contracts for Python Ruby 通过Brian McCallister的DesignByContract Ruby DBC ruby contract或contracts ruby Rust 通过contracts 16 crate Tcl 通过XOTcl 英语 XOTcl 面向对象扩展 参考文献 编辑 Bright Walter D Programming Language Contract Programming Digital Mars 2014 11 01 2014 11 10 原始内容存档于2014 11 28 Hodges Nick Write Cleaner Higher Quality Code with Class Contracts in Delphi Prism Embarcadero Technologies 20 January 2016 原始内容存档于2021 04 26 Findler Felleisen Contracts for Higher Order Functions 页面存档备份 存于互联网档案馆 Scala Standard Library Docs Assertions EPFL 2019 05 24 原始内容存档于2019 12 25 Strong typing as another contract enforcing in Scala see discussion at scala lang org 页面存档备份 存于互联网档案馆 DBC C 页面存档备份 存于互联网档案馆 Design by contract for C Code Contracts msdn microsoft com 2022 03 02 原始内容存档于2022 06 04 dbc 2022 03 02 原始内容存档于2022 06 04 gocontracts 2022 03 02 原始内容存档于2022 06 03 Contracts for Java 2022 03 02 原始内容存档于2022 03 03 Bean Validation specification beanvalidation org 2022 03 02 原始内容存档于2014 07 16 dbc code contracts 2022 03 02 原始内容存档于2021 11 04 macros 2022 03 02 原始内容存档于2022 06 06 PhpDeal 2022 03 02 原始内容存档于2022 06 04 deal 2022 03 02 原始内容存档于2022 06 13 contracts 2022 03 02 原始内容存档于2022 05 31 外部链接 编辑The Power of Design by Contract TM 页面存档备份 存于互联网档案馆 A top level description of DbC with links to additional resources Building bug free O O software An introduction to Design by Contract TM 页面存档备份 存于互联网档案馆 Older material on DbC Benefits and drawbacks implementation in RPS Obix Archive is的存檔 存档日期2013 02 01 Bertrand Meyer Applying Design by Contract 页面存档备份 存于互联网档案馆 IEEE Computer October 1992 Using Code Contracts for Safer Code 页面存档备份 存于互联网档案馆 取自 https zh wikipedia org w index php title 契约式设计 amp oldid 78953726, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。