《《契约式设计》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《契约式设计》PPT课件.ppt（85页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、契约式设计Design by Contract2023/1/11Institute of Computer SoftwareNanjing University摘要引言Eiffel 的 DbC 机制DbC与继承如何应用DbC2023/1/11Institute of Computer SoftwareNanjing University2引言Design by Contract (DbC)契约式设计方法学层面的思想以尽可能小的代价开发出可靠性出众的软件系统Eiffel语言的直接支持Bertrand Meyer：DbC是构建面向对象软件系统方法的核心！James McKim：“只要你会写程序，你
2、就会写契约”2023/1/11Institute of Computer SoftwareNanjing University3引言A discipline of analysis,design,implementation,management（可以贯穿于软件创建的全过程，从分析到设计，从文档到调试，甚至可以渗透到项目管理中）Viewing the relationship between a class and its clients as a formal agreement,expressing each partys rights and obligations.（把类和它的客户程序
3、之间的关系看做正式的协议，描述双方的权利和义务）2023/1/11Institute of Computer SoftwareNanjing University4引言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 elements contract.The contract of any software element should be
4、Explicit.Part of the software element itself.2023/1/11Institute of Computer SoftwareNanjing University5A human contract2023/1/11Institute of Computer SoftwareNanjing University6ClientSupplier(Satisfy precondition:)Bring package before 4 p.m.;pay fee.(Satisfy postcondition:)Deliver package by 10 a.m.
5、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.BENEFITS(权益/权利)deliverA view of software constructionConstructing systems as structured collections of cooperating s
6、oftware elements suppliers and clients cooperating on the basis of clear definitions of obligations and benefits.These definitions are the contracts.2023/1/11Institute of Computer SoftwareNanjing University7Properties of contractsA contract:Binds two parties(or more):supplier,client.Is explicit(writ
7、ten).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 p
8、ractices).2023/1/11Institute of Computer SoftwareNanjing University82023/1/11Institute of Computer SoftwareNanjing University9deferred class PLANE inheritAIRCRAFTfeaturestart_take_off is-Initiate take-off procedures.requirecontrols.passedassigned_runway.cleardeferredensureassigned_runway.owner=Curre
9、ntmovingendstart_landing,increase_altitude,decrease_altitude,moving,altitude,speed,time_since_take_off.Other features.invariant(time_since_take_off 10)endContracts for analysisPreconditionClass invariant-i.e.specified only.-not implemented.Postcondition2023/1/11Institute of Computer SoftwareNanjing
10、University10deferred class VAT inheritTANKfeaturein_valve,out_valve:VALVEfill is-Fill the vat.requirein_valve.openout_valve.closeddeferredensurein_valve.closedout_valve.closedis_fullendempty,is_full,is_empty,gauge,maximum,.Other features.invariantis_full=(gauge=0.97*maximum)and(gauge 5 n:=n+9 n 13Mo
11、st interesting properties:Strongest postcondition(from given precondition).Weakest precondition(from given postcondition).“P is stronger than or equal to Q”means:P implies QQUIZ:What is the strongest possible assertion?The weakest?2023/1/11Institute of Computer SoftwareNanjing University15Software c
12、orrectnessConsider P A QTake 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 True2023/1/11Institute of Computer SoftwareNanjing University16Strongest precond.Weakest postcond.“We are looking for someone
13、 whose work will be to start from initial situations as characterized by P,and deliver results as defined by Q摘要引言Eiffel 的的 DbC 机制机制DbC与继承如何应用DbC2023/1/11Institute of Computer SoftwareNanjing University17Design by Contract:The MechanismPreconditions and PostconditionsClass InvariantRun-time effect20
14、23/1/11Institute of Computer SoftwareNanjing University18A contract(from EiffelBase)2023/1/11Institute of Computer SoftwareNanjing University19extend(new:G;key:H)-Assuming there is no item of key key,-insert new with key;set inserted.requirekey_not_present:not has(key)ensureinsertion_done:item(key)=
15、newkey_present:has(key)inserted:insertedone_more:count=old count+1The contract2023/1/11Institute of Computer SoftwareNanjing University20ClientSupplierPRECONDITIONPOSTCONDITIONOBLIGATIONSPOSTCONDITIONPRECONDITIONBENEFITSRoutineA class without contractsclass ACCOUNT feature-Accessbalance:INTEGER-Bala
16、nceMinimum_balance:INTEGER is 1000-Minimum balancefeature NONE-Implementation of deposit and withdrawaladd(sum:INTEGER)is-Add sum to the balance(secret procedure).dobalance:=balance+sumend2023/1/11Institute of Computer SoftwareNanjing University21Without contracts(contd)2023/1/11Institute of Compute
17、r SoftwareNanjing University22feature-Deposit and withdrawal operationsdeposit(sum:INTEGER)is-Deposit sum into the account.doadd(sum)endwithdraw(sum:INTEGER)is-Withdraw sum from the account.doadd(sum)endmay_withdraw(sum:INTEGER):BOOLEAN is-Is it permitted to withdraw sum from the account?doResult:=(
18、balance-sum=Minimum_balance)endendIntroducing contractsclassclass ACCOUNT createcreatemakefeaturefeature NONE-Initializationmake(initial_amount:INTEGER)is is-Set up account with initial_amount.requirerequirelarge_enough:initial_amount=Minimum_balancedodobalance:=initial_amountensureensurebalance_set
19、:balance=initial_amountendend2023/1/11Institute of Computer SoftwareNanjing University23Introducing contracts(contd)2023/1/11Institute of Computer SoftwareNanjing University24feature-Accessbalance:INTEGER-BalanceMinimum_balance:INTEGER is 1000-Minimum balancefeature NONE-Implementation of deposit an
20、d withdrawaladd(sum:INTEGER)is-Add sum to the balance(secret procedure).dobalance:=balance+sumensureincreased:balance=old balance+sum endWith contracts(contd)2023/1/11Institute of Computer SoftwareNanjing University25feature-Deposit and withdrawal operations deposit(sum:INTEGER)is-Deposit sum into t
21、he account.requirenot_too_small:sum=0doadd(sum)ensureincreased:balance=old balance+sumendWith contracts(contd)withdraw(sum:INTEGER)is-Withdraw sum from the account.requirenot_too_small:sum=0not_too_big:sum=Minimum_balance)endinvariantnot_under_minimum:balance=Minimum_balanceend2023/1/11Institute of
22、Computer SoftwareNanjing University29The 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(.)2023/1/11Institute of Computer SoftwareNanjing University30The correctness o
23、f a classFor every creation procedure cp:precp docp postcp and INVFor 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.2023/1/11Inst
24、itute of Computer SoftwareNanjing University31a.f()a.g()a.f()create a.make()S1S2S3S4Examplebalance=deposits.total withdrawals.total2023/1/11Institute of Computer SoftwareNanjing University32depositswithdrawalsbalancedepositswithdrawals(A1)(A2)A more sophisticated version2023/1/11Institute of Compute
25、r SoftwareNanjing University33class ACCOUNT createmakefeature NONE-Implementationadd(sum:INTEGER)is-Add sum to the balance(secret procedure).dobalance:=balance+sumensurebalance_increased:balance=old balance+sum enddeposits:DEPOSIT_LISTwithdrawals:WITHDRAWAL_LISTNew version(contd)feature NONE-Initial
26、izationmake(initial_amount:INTEGER)is-Set up account with initial_amount.requirelarge_enough:initial_amount=Minimum_balancedo balance:=initial_amountcreate deposits.makecreate withdrawals.makeensurebalance_set:balance=initial_amountendfeature-Accessbalance:INTEGER-BalanceMinimum_balance:INTEGER is 1
27、000-Minimum balance2023/1/1134New version(contd)feature-Deposit and withdrawal operations deposit(sum:INTEGER)is-Deposit sum into the account.requirenot_too_small:sum=0doadd(sum)deposits.extend(create DEPOSIT.make(sum)ensureincreased:balance=old balance+sumend2023/1/11Institute of Computer SoftwareN
28、anjing University35New version(contd)2023/1/11Institute of Computer SoftwareNanjing University36withdraw(sum:INTEGER)is-Withdraw sum from the account.requirenot_too_small:sum=0not_too_big:sum=Minimum_balance)endinvariantnot_under_minimum:balance=Minimum_balanceconsistent:balance=deposits.total withd
29、rawals.totalendThe correctness of a classFor every creation procedure cp:precp docp postcp and INVFor every exported routine r:INV and prer dor postr and INV2023/1/11Institute of Computer SoftwareNanjing University38a.f()a.g()a.f()create a.make()S1S2S3S4Initial version2023/1/11Institute of Computer
30、SoftwareNanjing University39featurefeature NONE-Initializationmake(initial_amount:INTEGER)is is-Set up account with initial_amount.requirerequire large_enough:initial_amount=Minimum_balancedodobalance:=initial_amount createcreate deposits.makecreatecreate withdrawals.makeensureensurebalance_set:bala
31、nce=initial_amount end endCorrect version2023/1/11Institute of Computer SoftwareNanjing University40featurefeature NONE-Initializationmake(initial_amount:INTEGER)is is-Set up account with initial_amount.requirerequirelarge_enough:initial_amount=Minimum_balancedodocreatecreate deposits.makecreatecrea
32、te withdrawals.makedeposit(initial_amount)ensureensurebalance_set:balance=initial_amountendend40Contracts:run-time effectCompilation options(per class,in Eiffel):No assertion checking Preconditions only Preconditions and postconditions Preconditions,postconditions,class invariants All assertions2023
33、/1/11Institute of Computer SoftwareNanjing University4141摘要引言Eiffel 的 DbC 机制DbC与继承与继承如何应用DbC2023/1/11Institute of Computer SoftwareNanjing University42继承与 Design by Contract问题：子类中的断言与父类中的断言是什么关系？依据子类乃父类的特化，子类的实例也是父类的合法实例。申明为父类的引用运行时可能指向子类实例因而？2023/1/11Institute of Computer SoftwareNanjing University
34、43Inheritance and assertions2023/1/11Institute of Computer SoftwareNanjing University44Correct call:if a1.thena1.r(.)else.endr isensurer isensureCABa1:Aa1.r()Contract2023/1/11Institute of Computer SoftwareNanjing University45ClientSupplier(Satisfy precondition:)不得要求投递超过5kg的包裹(Satisfy postcondition:)
35、在3个工作日内投送到位OBLIGATIONS(From postcondition:)3个工作日内包裹到位(From precondition:)不受理超过5kg的包裹BENEFITSdeliveryContractclass COURIER feature deliver(p:Package,d:Destination)require -包裹重量不超过5kg ensure -3个工作日内投送到指定地点 end2023/1/11Institute of Computer SoftwareNanjing University46More desirable contract2023/1/11In
36、stitute of Computer SoftwareNanjing University47ClientSupplier(Satisfy precondition:)不得要求投递超过8kg的包裹(Satisfy postcondition:)在2个工作日内投送到位OBLIGATIONS(From postcondition:)2个工作日内包裹到位(From precondition:)不受理超过8kg的包裹BENEFITSdeliveryMore desirable contractclass DIFFERENT_COURIERInherit COURIERredefine deliver
37、 feature deliver(p:Package,d:Destination)require -包裹重量不超过5kg require else -包裹重量不超过8kg ensure -3天内投送到指定地点 ensure then -2天内投送到指定地点 end2023/1/11Institute of Computer SoftwareNanjing University48require -包裹重量不超过8kgensure -2天内投送到指定地点Assertion redeclaration ruleRedefined version may not have require or en
38、sure.May have nothing(assertions kept by default),orrequire else new_preensure then new_postResulting assertions are:original_precondition or new_preoriginal_postcondition and new_post2023/1/11Institute of Computer SoftwareNanjing University49Invariant accumulationEvery class inherits all the invari
39、ant clauses of its parents.These clauses are conceptually“and”-ed.2023/1/11Institute of Computer SoftwareNanjing University50简言之可以使用require else削弱先验条件可以使用ensure then加强后验条件用and把不变式子句和你所继承的不变式子句结合起来，就可以加强不变式2023/1/11Institute of Computer SoftwareNanjing University51摘要引言Eiffel 的 DbC 机制DbC与继承如何应用如何应用DbC
40、其它 2023/1/11Institute of Computer SoftwareNanjing University52Design by Contract:How to apply目的：构造高质量的程序理解Contract violationDbC与Quality Assurance（QA）Precondition DesignNot defensive programmingClass Invariants and business logic2023/1/11Institute of Computer SoftwareNanjing University53What are cont
41、racts 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 o
42、f libraries).Exception handling.2023/1/11Institute of Computer SoftwareNanjing University54Some 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
43、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.2023/1/11Institute of Computer SoftwareNanjing University55Some benefits:managerialLibrary users can trust docu
44、mentation.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,manag
45、ers,potentially customers.Component-based development possible on a solid basis.2023/1/11Institute of Computer SoftwareNanjing University56A 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 ru
46、n-time assertion violation is something else:the manifestation ofA DEFECT(“BUG”)2023/1/11Institute of Computer SoftwareNanjing University57Contracts and quality assurancePrecondition violation:Bug in the client.Postcondition violation:Bug in the supplier.Invariant violation:Bug in the supplier.P A Q
47、2023/1/11Institute of Computer SoftwareNanjing University58Contracts and bug typesPreconditions are particularly useful to find bugs in client code:2023/1/11Institute of Computer SoftwareNanjing University59YOUR APPLICATIONCOMPONENT LIBRARYyour_list.insert(y,a+b+1)i=0class LIST GContracts and qualit
48、y 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 assertions2023/1/11Institute of Computer SoftwareNanjing Univ
49、ersity60Contracts 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 softwa
50、re 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,19972023/1/11Institute of