• 1. 2018/10/23Institute of Computer Software Nanjing University1Design by Contract契约式设计
  • 2. 2018/10/23Institute of Computer Software Nanjing University2摘要引言 软件正确性 Eiffel 的 DbC 机制 如何应用DbC 其它
  • 3. 2018/10/23Institute of Computer Software Nanjing University3引言“To program is to understand” -- Kristen Nygaard “Scientific reasoning is nothing but the result of starting from ordinary observations and continuing with simple deductions -- only very patiently and stubbornly”
  • 4. 2018/10/23Institute of Computer Software Nanjing University4引言Design by Contract 契约式设计 DbC 方法学层面的思想 Eiffel语言的直接支持 从“技艺”到“科学”的努力 信仰与现实 “革命尚未成功,同志仍须努力!”
  • 5. 2018/10/23Institute of Computer Software Nanjing University5引言A discipline of analysis, design, implementation, management Viewing the relationship between a class and its clients as a formal agreement, expressing each party’s rights and obligations.
  • 6. 2018/10/23Institute of Computer Software Nanjing University6引言Every software element is intended to satisfy a certain goal, for the benefit of other software elements (and ultimately of human users). This goal is the element’s contract. The contract of any software element should be Explicit. Part of the software element itself.
  • 7. 7A human contractClientSupplier(Satisfy precondition:) Bring package before 4 p.m.; pay fee.(Satisfy postcondition:) Deliver package by 10 a.m. next day.OBLIGATIONS(From postcondition:) Get package delivered by 10 a.m. next day.(From precondition:) Not required to do anything if package delivered after 4 p.m., or fee not paid.BENEFITSdeliver
  • 8. 8A view of software constructionConstructing systems as structured collections of cooperating software elements — suppliers and clients — cooperating on the basis of clear definitions of obligations and benefits. These definitions are the contracts.
  • 9. 9Properties of contractsA contract: Binds two parties (or more): supplier, client. Is explicit (written). Specifies mutual obligations and benefits. Usually maps obligation for one of the parties into benefit for the other, and conversely. Has no hidden clauses: obligations are those specified. Often relies, implicitly or explicitly, on general rules applicable to all contracts (laws, regulations, standard practices).
  • 10. 10deferred class PLANE inherit AIRCRAFT feature start_take_off is -- Initiate take-off procedures. require controls.passed assigned_runway.clear deferred ensure assigned_runway.owner = Current moving end start_landing, increase_altitude, decrease_altitude, moving, altitude, speed, time_since_take_off ... [Other features] ... invariant (time_since_take_off <= 20) implies (assigned_runway.owner = Current) moving = (speed > 10) endContracts for analysisPreconditionClass invariant-- i.e. specified only. -- not implemented.Postcondition
  • 11. 11deferred class VAT inherit TANK feature in_valve, out_valve: VALVE fill is -- Fill the vat. require in_valve.open out_valve.closed deferred ensure in_valve.closed out_valve.closed is_full end empty, is_full, is_empty, gauge, maximum, ... [Other features] ... invariant is_full = (gauge >= 0.97 * maximum)  and  (gauge <= 1.03 * maximum) endContracts for analysis (cont’d)PreconditionClass invariant-- i.e. specified only. -- not implemented.Postcondition
  • 12. 12Contracts for analysis (cont’d)ClientSupplier(Satisfy precondition:) Make sure input valve is open, output valve is closed.(Satisfy postcondition:) Fill the vat and close both valves.OBLIGATIONS(From postcondition:) Get filled-up vat, with both valves closed.(From precondition:) Simpler processing thanks to assumption that valves are in the proper initial position.BENEFITSfill
  • 13. 13So, is it like “assert.h”?(Source: Reto Kramer) Design by Contract goes further: “Assert” does not provide a contract. Clients cannot see asserts as part of the interface. Asserts do not have associated semantic specifications. Not explicit whether an assert represents a precondition, post-conditions or invariant. Asserts do not support inheritance. Asserts do not yield automatic documentation.
  • 14. 2018/10/23Institute of Computer Software Nanjing University14Design by Contract引言 软件正确性与Hoare Triple Eiffel 的 DbC 机制 如何应用 DbC 其它
  • 15. 15软件的正确性与Hoare TripleCorrectness is a relative notion: consistency of implementation vis-à-vis specification. (This assumes there is a specification!) Basic notation: (P, Q: assertions, i.e. properties of the state of the computation. A: instructions). {P} A {Q} “Hoare triple” What this means (total correctness): Any execution of A started in a state satisfying P will terminate in a state satisfying Q.
  • 16. 16Hoare triples: a simple example {n > 5} n := n + 9 {n > 13} Most interesting properties: Strongest postcondition (from given precondition). Weakest precondition (from given postcondition). “P is stronger than or equal to Q” means: P implies Q QUIZ: What is the strongest possible assertion? The weakest?
  • 17. 17Specifying a square root routine{x >= 0} ... Square root algorithm to compute y ... {abs (y ^ 2 – x) <= 2 * epsilon * y} -- i.e.: y approximates exact square root of x -- within epsilon
  • 18. 18软件的正确性与Hoare TripleConsider {P} A {Q} Take this as a job ad in the classifieds. Should a lazy employment candidate hope for a weak or strong P? What about Q? Two special offers: 1. {False} A {...} 2. {...} A {True}
  • 19. 2018/10/23Institute of Computer Software Nanjing University19Design by Contract引言 软件正确性 Eiffel 的 DbC 机制 如何应用 DbC 其它
  • 20. 2018/10/23Institute of Computer Software Nanjing University20Design by Contract: The MechanismPreconditions and Postconditions Class Invariant Run-time effect
  • 21. 21A contract (from EiffelBase) extend (new: G; key: H) -- Assuming there is no item of key key, -- insert new with key; set inserted. require key_not_present: not has (key) ensure insertion_done: item (key) = new key_present: has (key) inserted: inserted one_more: count = old count + 1
  • 22. 22The contractClientSupplierPRECONDITIONPOSTCONDITIONOBLIGATIONSPOSTCONDITIONPRECONDITIONBENEFITSRoutine
  • 23. 23A class without contractsclass ACCOUNT feature -- Access balance: INTEGER -- Balance Minimum_balance: INTEGER is 1000 -- Minimum balance feature {NONE} -- Implementation of deposit and withdrawal add (sum: INTEGER) is -- Add sum to the balance (secret procedure). do balance := balance + sum end
  • 24. 24Without contracts (cont’d)feature -- Deposit and withdrawal operations deposit (sum: INTEGER) is -- Deposit sum into the account. do add (sum) end withdraw (sum: INTEGER) is -- Withdraw sum from the account. do add (– sum) end may_withdraw (sum: INTEGER): BOOLEAN is -- Is it permitted to withdraw sum from the account? do Result := (balance - sum >= Minimum_balance) end end
  • 25. 25Introducing contractsclass ACCOUNT create make feature {NONE} -- Initialization make (initial_amount: INTEGER) is -- Set up account with initial_amount. require large_enough: initial_amount >= Minimum_balance do balance := initial_amount ensure balance_set: balance = initial_amount end
  • 26. 26Introducing contracts (cont’d)feature -- Access balance: INTEGER -- Balance Minimum_balance: INTEGER is 1000 -- Minimum balance feature {NONE} -- Implementation of deposit and withdrawal add (sum: INTEGER) is -- Add sum to the balance (secret procedure). do balance := balance + sum ensure increased: balance = old balance + sum end
  • 27. 27With contracts (cont’d)feature -- Deposit and withdrawal operations deposit (sum: INTEGER) is -- Deposit sum into the account. require not_too_small: sum >= 0 do add (sum) ensure increased: balance = old balance + sum end
  • 28. 28With contracts (cont’d) withdraw (sum: INTEGER) is -- Withdraw sum from the account. require not_too_small: sum >= 0 not_too_big: sum <= balance – Minimum_balance do add (– sum) -- i.e. balance := balance – sum ensure decreased: balance = old balance - sum end
  • 29. 29The contractClientSupplier(Satisfy precondition:) Make sure sum is neither too small nor too big.(Satisfy postcondition:) Update account for withdrawal of sum.OBLIGATIONS(From postcondition:) Get account updated with sum withdrawn.(From precondition:) Simpler processing: may assume sum is within allowable bounds.BENEFITSwithdraw
  • 30. 30The imperative and the applicativedo balance := balance - sumensure balance = old balance - sum PRESCRIPTIVE DESCRIPTIVE How? Operational Implementation Command Instruction Imperative What? Denotational Specification Query Expression Applicative
  • 31. 31With contracts (end) may_withdraw (sum: INTEGER): BOOLEAN is -- Is it permitted to withdraw sum from the -- account? do Result := (balance - sum >= Minimum_balance) end invariant not_under_minimum: balance >= Minimum_balance end
  • 32. 32The class invariantConsistency constraint applicable to all instances of a class. Must be satisfied: After creation. After execution of any feature by any client. (Qualified calls only: a.f (...))
  • 33. 33The correctness of a class For every creation procedure cp: {precp} docp {postcp and INV} For every exported routine r: {INV and prer} dor {postr and INV} The worst possible erroneous run-time situation in object-oriented software development: Producing an object that does not satisfy the invariant of its own class. a.f (…)a.g (…)a.f (…)create a.make (…)S1S2S3S4
  • 34. 34Uniform Access balance = deposits.total –withdrawals.totaldepositswithdrawalsbalancedepositswithdrawals(A1)(A2)
  • 35. 35class ACCOUNT create make feature {NONE} -- Implementation add (sum: INTEGER) is -- Add sum to the balance (secret procedure). do balance := balance + sum ensure balance_increased: balance = old balance + sum end deposits: DEPOSIT_LIST withdrawals: WITHDRAWAL_LISTA more sophisticated version
  • 36. 36feature {NONE} -- Initialization make (initial_amount: INTEGER) is -- Set up account with initial_amount. require large_enough: initial_amount >= Minimum_balance do balance := initial_amount create deposits.make create withdrawals.make ensure balance_set: balance = initial_amount end feature -- Access balance: INTEGER -- Balance Minimum_balance: INTEGER is 1000 -- Minimum balanceNew version (cont’d)
  • 37. 37New version (cont’d)feature -- Deposit and withdrawal operations deposit (sum: INTEGER) is -- Deposit sum into the account. require not_too_small: sum >= 0 do add (sum) deposits.extend (create {DEPOSIT}.make (sum)) ensure increased: balance = old balance + sum end
  • 38. 38New version (cont’d) withdraw (sum: INTEGER) is -- Withdraw sum from the account. require not_too_small: sum >= 0 not_too_big: sum <= balance – Minimum_balance do add (– sum) withdrawals.extend (create {WITHDRAWAL}.make (sum)) ensure decreased: balance = old balance – sum one_more: withdrawals.count = old withdrawals.count + 1 end
  • 39. 39New version (end) may_withdraw (sum: INTEGER): BOOLEAN is -- Is it permitted to withdraw sum from the -- account? do Result := (balance - sum >= Minimum_balance) end invariant not_under_minimum: balance >= Minimum_balance consistent: balance = deposits.total – withdrawals.total end
  • 40. 40The correctness of a class For every creation procedure cp: {precp} docp {postcp and INV} For every exported routine r: {INV and prer} dor {postr and INV} a.f (…)a.g (…)a.f (…)create a.make (…)S1S2S3S4
  • 41. 41feature {NONE} -- Initialization make (initial_amount: INTEGER) is -- Set up account with initial_amount. require large_enough: initial_amount >= Minimum_balance do balance := initial_amount create deposits.make create withdrawals.make ensure balance_set: balance = initial_amount endInitial version
  • 42. 42feature {NONE} -- Initialization make (initial_amount: INTEGER) is -- Set up account with initial_amount. require large_enough: initial_amount >= Minimum_balance do create deposits.make create withdrawals.make deposit (initial_amount) ensure balance_set: balance = initial_amount endCorrect version
  • 43. 43Contracts: run-time effectCompilation options (per class, in Eiffel): No assertion checking Preconditions only Preconditions and postconditions Preconditions, postconditions, class invariants All assertions
  • 44. 44The contract languageLanguage of boolean expressions (plus old): No predicate calculus (i.e. no quantifiers,  or ). Function calls permitted (e.g. in a STACK class):put (x: G) is -- Push x on top of stack. require not is_full do … ensure not is_empty endremove (x: G) is -- Pop top of stack. require not is_empty do … ensure not is_full end
  • 45. 45The contract language (cont’d)First order predicate calculus may be desirable, but not sufficient anyway. Example: “The graph has no cycles”. In assertions, use only side-effect-free functions. Use of iterators provides the equivalent of first-order predicate calculus in connection with a library such as EiffelBase or STL. For example (Eiffel agents, i.e. routine objects): my_integer_list.for_all (agent is_positive (?)) with is_positive (x: INTEGER): BOOLEAN is do Result := (x > 0) end
  • 46. 46The imperative and the applicativedo balance := balance - sumensure balance = old balance - sum PRESCRIPTIVE DESCRIPTIVE How? Operational Implementation Command Instruction Imperative What? Denotational Specification Query Expression Applicative
  • 47. 2018/10/23Institute of Computer Software Nanjing University47继承与 Design by Contract问题: 子类中的断言与父类中的断言是什么关系? 依据 子类乃父类的特化,子类的实例也是父类的合法实例。 申明为父类的引用运行时可能指向子类实例 因而 ?
  • 48. 48Inheritance and assertions Correct call: if a1. then a1.r (...) else ... endr isrequireensurer isrequireensureCABa1: Aa1.r (…)…
  • 49. 49Redefined version may not have require or ensure. May have nothing (assertions kept by default), or require else new_pre ensure then new_post Resulting assertions are: original_precondition or new_pre original_postcondition and new_postAssertion redeclaration rule
  • 50. 50Invariant accumulationEvery class inherits all the invariant clauses of its parents. These clauses are conceptually “and”-ed.
  • 51. 51Some benefits: technicalDevelopment process becomes more focused. Writing to spec. Sound basis for writing reusable software. Exception handling guided by precise definition of “normal” and “abnormal” cases. Interface documentation always up-to-date, can be trusted. Documentation generated automatically. Faults occur close to their cause. Found faster and more easily. Guide for black-box test case generation.
  • 52. 52Some benefits: managerialLibrary users can trust documentation. They can benefit from preconditions to validate their own software. Test manager can benefit from more accurate estimate of test effort. Black-box specification for free. Designers who leave bequeath not only code but intent. Common vocabulary between all actors of the process: developers, managers, potentially customers. Component-based development possible on a solid basis.
  • 53. 2018/10/23Institute of Computer Software Nanjing University53Design by Contract引言 软件正确性 Eiffel 的 DbC 机制 如何应用 DbC 其它
  • 54. 2018/10/23Institute of Computer Software Nanjing University54Design by Contract: How to apply目的:构造高质量的程序 理解Contract violation DbC与QA Precondition Design No defensive programming Class Invariants and business logic
  • 55. 55What are contracts good for?Writing correct software (analysis, design, implementation, maintenance, reengineering). Documentation (the “contract” form of a class). Effective reuse. Controlling inheritance. Preserving the work of the best developers. Quality assurance, testing, debugging (especially in connection with the use of libraries) . Exception handling .
  • 56. 56A contract violation is not a special caseFor special cases (e.g. “if the sum is negative, report an error...”) use standard control structures (e.g. if ... then ... else...). A run-time assertion violation is something else: the manifestation of A DEFECT (“BUG”)
  • 57. 57Contracts and quality assurancePrecondition violation: Bug in the client. Postcondition violation: Bug in the supplier. Invariant violation: Bug in the supplier. {P} A {Q}
  • 58. 58Contracts and bug typesPreconditions are particularly useful to find bugs in client code: YOUR APPLICATION COMPONENT LIBRARYyour_list.insert (y, a + b + 1)i <= count + 1insert (x: G; i: INTEGER) isrequirei >= 0class LIST [G]…
  • 59. 59Contracts and quality assuranceUse run-time assertion monitoring for quality assurance, testing, debugging. Compilation options (reminder): No assertion checking Preconditions only Preconditions and postconditions Preconditions, postconditions, class invariants All assertions
  • 60. 60Contracts missedAriane 5 (see Jézéquel & Meyer, IEEE Computer, January 1997) Lunar Orbiter Vehicle Failure of air US traffic control system, November 2000 Y2K etc. etc. etc.
  • 61. 61Contracts and quality assuranceContracts enable QA activities to be based on a precise description of what they expect. Profoundly transform the activities of testing, debugging and maintenance. “I believe that the use of Eiffel-like module contracts is the most important non-practice in software world today. By that I mean there is no other candidate practice presently being urged upon us that has greater capacity to improve the quality of software produced. ... This sort of contract mechanism is the sine-qua-non of sensible software reuse. ”                       Tom de Marco, IEEE Computer, 1997
  • 62. 62Contract monitoringEnabled or disabled by compile-time options. Default: preconditions only. In development: use “all assertions” whenever possible. During operation: normally, should disable monitoring. But have an assertion-monitoring version ready for shipping. Result of an assertion violation: exception. Ideally: static checking (proofs) rather than dynamic monitoring.
  • 63. 63Contracts and documentationRecall example class: class ACCOUNT create make feature {NONE} -- Implementation add (sum: INTEGER) is -- Add sum to the balance (secret procedure). do balance := balance + sum ensure increased: balance = old balance + sum end deposits: DEPOSIT_LIST withdrawals: WITHDRAWAL_LIST
  • 64. 64Class example (cont’d)feature {NONE} -- Initialization make (initial_amount: INTEGER) is -- Set up account with initial_amount. require large_enough: initial_amount >= Minimum_balance do create deposits.make create withdrawals.make deposit (initial_amount) ensure balance_set: balance = initial_amount end feature -- Access balance: INTEGER -- Balance Minimum_balance: INTEGER is 1000 -- Minimum balance
  • 65. 65Class example (cont’d)feature -- Deposit and withdrawal operations deposit (sum: INTEGER) is -- Deposit sum into the account. require not_too_small: sum >= 0 do add (sum) deposits.extend (create {DEPOSIT}.make (sum)) ensure increased: balance = old balance + sum end
  • 66. 66Class example (cont’d) withdraw (sum: INTEGER) is -- Withdraw sum from the account. require not_too_small: sum >= 0 not_too_big: sum <= balance – Minimum_balance do add (– sum) withdrawals.extend (create {WITHDRAWAL}.make (sum)) ensure decreased: balance = old balance – sum one_more: withdrawals.count = old withdrawals.count + 1 end
  • 67. 67Class example (end) may_withdraw (sum: INTEGER): BOOLEAN is -- Is it permitted to withdraw sum from the -- account? do Result := (balance - sum >= Minimum_balance) end invariant not_under_minimum: balance >= Minimum_balance consistent: balance = deposits.total – withdrawals.total end
  • 68. 68Contract form: DefinitionSimplified form of class text, retaining interface elements only: Remove any non-exported (private) feature. For the exported (public) features: Remove body (do clause). Keep header comment if present. Keep contracts: preconditions, postconditions, class invariant. Remove any contract clause that refers to a secret feature. (This raises a problem; can you see it?)
  • 69. 69Export rule for preconditionsIn some_property must be exported (at least) to A, B and C! No such requirement for postconditions and invariants. feature {A, B, C} r (…) is require some_property
  • 70. 70Contract form of ACCOUNT classclass interface ACCOUNT create make feature balance: INTEGER -- Balance Minimum_balance: INTEGER is 1000 -- Minimum balance deposit (sum: INTEGER) -- Deposit sum into the account. require not_too_small: sum >= 0 ensure increased: balance = old balance + sum
  • 71. 71Contract form (cont’d) withdraw (sum: INTEGER) -- Withdraw sum from the account. require not_too_small: sum >= 0 not_too_big: sum <= balance – Minimum_balance ensure decreased: balance = old balance – sum one_more: withdrawals.count = old withdrawals.count + 1 may_withdraw (sum: INTEGER): BOOLEAN -- Is it permitted to withdraw sum from the -- account? invariant not_under_minimum: balance >= Minimum_balance consistent: balance = deposits.total – withdrawals.total end
  • 72. 72Flat, interfaceFlat form of a class: reconstructed class with all the features at the same level (immediate and inherited). Takes renaming, redefinition etc. into account. The flat form is an inheritance-free client-equivalent form of the class. Interface form: the contract form of the flat form. Full interface documentation.
  • 73. 73Uses of the contract and interface formsDocumentation, manuals Design Communication between developers Communication between developers and managers
  • 74. 74Contracts and reuseThe contract form — i.e. the set of contracts governing a class — should be the standard form of library documentation. Reuse without a contract is sheer folly. See the Ariane 5 example. See Jézéquel & Meyer, IEEE Computer, January 1997.
  • 75. 75Methodological notesContracts are not input checking tests... ... but they can be used to help weed out undesirable input. Filter modules: External objects Input and validation modules Processing modulesPreconditions here only
  • 76. 76Precondition designThe client must guarantee the precondition before the call. This does not necessarily mean testing for the precondition. Scheme 1 (testing): if not my_stack.is_full then my_stack.put (some_element) end Scheme 2 (guaranteeing without testing): my_stack.remove ... my_stack.put (some_element)
  • 77. 77Another examplesqrt (x, epsilon: REAL): REAL is -- Square root of x, precision epsilon require x >= 0 epsilon >= 0 do ... ensure abs (Result ^ 2 – x) <= 2 * epsilon * Result end
  • 78. 78The contractClientSupplier(Satisfy precondition:) Provide non-negative value and precision that is not too small.(Satisfy postcondition:) Produce square root within requested precision.OBLIGATIONS(From postcondition:) Get square root within requested precision.(From precondition:) Simpler processing thanks to assumptions on value and precision.BENEFITSsqrt
  • 79. 79Not defensive programming!It is never acceptable to have a routine of the form sqrt (x, epsilon: REAL): REAL is -- Square root of x, precision epsilon require x >= 0 epsilon >= 0 do if x < 0 then … Do something about it (?) … else … normal square root computation … end ensure abs (Result ^ 2 – x) <= 2 * epsilon * Result end
  • 80. 80Not defensive programmingFor every consistency condition that is required to perform a certain operation: Assign responsibility for the condition to one of the contract’s two parties (supplier, client). Stick to this decision: do not duplicate responsibility. Simplifies software and improves global reliability.
  • 81. 81Interpretersclass BYTECODE_PROGRAM feature verified: BOOLEAN trustful_execute (program: BYTECODE) is require ok: verified do ... end distrustful_execute (program: BYTECODE) is do verify if verified then trustful_execute (program) end end verify is do ... end end
  • 82. 82How strong should a precondition be?Two opposite styles: Tolerant: weak preconditions (including the weakest, True: no precondition). Demanding: strong preconditions, requiring the client to make sure all logically necessary conditions are satisfied before each call. Partly a matter of taste. But: demanding style leads to a better distribution of roles, provided the precondition is: Justifiable in terms of the specification only. Documented (through the short form). Reasonable!
  • 83. 83A demanding stylesqrt (x, epsilon: REAL): REAL is -- Square root of x, precision epsilon -- Same version as before require x >= 0 epsilon >= 0 do ... ensure abs (Result ^ 2 – x) <= 2 * epsilon * Result end
  • 84. 84 sqrt (x, epsilon: REAL): REAL is -- Square root of x, precision epsilon require True do if x < 0 then … Do something about it (?) … else … normal square root computation … computed := True end ensure computed implies abs (Result ^ 2 – x) <= 2 * epsilon * Result endA tolerant style NO INPUT TOO BIG OR TOO SMALL!
  • 85. 85Contrasting styles put (x: G) is -- Push x on top of stack. require not is_full do .... end tolerant_put (x: G) is -- Push x if possible, otherwise set impossible to -- True. do if not is_full then put (x) else impossible := True end end
  • 86. 86Invariants and business rulesInvariants are absolute consistency conditions. They can serve to represent business rules if knowledge is to be built into the software. Form 1 invariant not_under_minimum: balance >= Minimum_balance Form 2 invariant not_under_minimum_if_normal: normal_state implies (balance >= Minimum_balance)
  • 87. 2018/10/23Institute of Computer Software Nanjing University87几条基本原则区分命令和查询; 区分基本查询和派生查询; 为每个派生查询设定一个后置条件,用一个或多个基本查询定义之; 对于每个命令设定一个后置条件,规定每个基本查询的值; 对于每个查询和命令,给以必要的前置条件; 撰写不变式定义对象的恒定特性。
  • 88. 2018/10/23Institute of Computer Software Nanjing University88更多tips在适当地方添加物理限制 (non-void?) 前置条件中尽量使用高效的查询 如有必要增加高效派生查询,并以后置条件保证其与原低效查询之间的等价关系 用不变式限定属性 若派生查询实现为属性
  • 89. 2018/10/23Institute of Computer Software Nanjing University89更多tips为支持重定义,用相应的前置条件确保每个后置条件 (old precondition) implies original_postcondition 框定规则:对(很多时候隐式的)不变的显式说明 若有保密问题,秘密的查询可在契约中使用,而后设为私有(可能有CATCALL问题?)。
  • 90. 2018/10/23Institute of Computer Software Nanjing University90Design by Contract引言 软件正确性 Eiffel 的 DbC 机制 如何应用 DbC 其它
  • 91. 91Loop troubleLoops are needed, powerful But very hard to get right: “off-by-one” Infinite loops Improper handling of borderline cases For example: binary search feature
  • 92. 92The answer: assertionsUse of loop variants and invariants. A loop is a way to compute a certain result by successive approximations. (e.g. computing the maximum value of an array of integers)
  • 93. 93Computing the max of an arrayApproach by successive slices: max_of_array (t: ARRAY [INTEGER]): INTEGER is -- Maximum value of array t local i: INTEGER do from i := t.lower Result := t @ lower until i = t.upper loop i := i + 1 Result := Result.max (t @ i) end end
  • 94. 94Loop variants and invariantsSyntax: from init invariant inv -- Correctness property variant var -- Ensure loop termination. until exit loop body end
  • 95. 95Maximum of an array (cont’d) max_of_array (t: ARRAY [INTEGER]): INTEGER is -- Maximum value of array t local i: INTEGER do from i := t.lower Result := t @ lower invariant -- Result is the max of the elements of t at indices -- t.lower to i variant t.lower - i until i = t.upper loop i := i + 1 Result := Result.max (t @ i) end end
  • 96. 96A powerful assertion languageAssertion language: Not first-order predicate calculus But powerful through: Function calls Even allows to express: Loop properties
  • 97. 97Another one…Check instruction: ensure that a property is True at a certain point of the routine execution. E.g. Tolerant style example: Adding a check clause for readability.
  • 98. 98Precondition designScheme 2 (guaranteeing without testing): my_stack.remove check my_stack_not_full: not my_stack.is_full end my_stack.put (some_element)
  • 99. 小结DbC 原理 借鉴“契约”原理,界定模块之间的权利义务,规范软件的开发,提高软件质量。 设施 优势99
  • 100. 作业-7请给出作业2中银行帐户类型的带Contract的类Account。(请使用Java和Contract4J5,并给出相应的JUnit测试集) 在DbC下,何谓一个类相对于其契约是正确的?为什么说再入(reentrance)是一种很容易导致错误的行为? 子类契约与其父类契约是何种关系?若父类预计到子类将重定义其某个方法,且有可能需要弱化前置条件以扩大处理能力,且在扩大的处理后需弱化后置条件,应如何处理才能使得既不损害父类的契约,又给子类的扩展留下空间?(如父类是一个列表,put(x)方法的前置条件为x不属于这个列表,后置条件为x属于这个列表,且列表元素个数加了1;而子类想放宽前置条件,可以接受x已在列表中,只不过此时什么都不做,这样显然列表元素不变)。2018/10/23Institute of Computer Software Nanjing University100