最新契约式设计ppt课件.ppt

《最新契约式设计ppt课件.ppt》由会员分享，可在线阅读，更多相关《最新契约式设计ppt课件.ppt（86页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。

1、进入夏天，少不了一个热字当头，电扇空调陆续登场，每逢此时，总会想起进入夏天，少不了一个热字当头，电扇空调陆续登场，每逢此时，总会想起那一把蒲扇。蒲扇，是记忆中的农村，夏季经常用的一件物品。记忆中的故那一把蒲扇。蒲扇，是记忆中的农村，夏季经常用的一件物品。记忆中的故乡，每逢进入夏天，集市上最常见的便是蒲扇、凉席，不论男女老少，个个手持乡，每逢进入夏天，集市上最常见的便是蒲扇、凉席，不论男女老少，个个手持一把，忽闪忽闪个不停，嘴里叨叨着一把，忽闪忽闪个不停，嘴里叨叨着“怎么这么热怎么这么热”，于是三五成群，聚在大树，于是三五成群，聚在大树下，或站着，或随即坐在石头上，手持那把扇子，边唠嗑边乘凉。孩

2、子们却在周下，或站着，或随即坐在石头上，手持那把扇子，边唠嗑边乘凉。孩子们却在周围跑跑跳跳，热得满头大汗，不时听到围跑跑跳跳，热得满头大汗，不时听到“强子，别跑了，快来我给你扇扇强子，别跑了，快来我给你扇扇”。孩。孩子们才不听这一套，跑个没完，直到累气喘吁吁，这才一跑一踮地围过了，这时子们才不听这一套，跑个没完，直到累气喘吁吁，这才一跑一踮地围过了，这时母亲总是，好似生气的样子，边扇边训，母亲总是，好似生气的样子，边扇边训，“你看热的，跑什么？你看热的，跑什么？”此时这把蒲扇，此时这把蒲扇，是那么凉快，那么的温馨幸福，有母亲的味道！蒲扇是中国传统工艺品，在是那么凉快，那么的温馨幸福，有母亲的味

3、道！蒲扇是中国传统工艺品，在我国已有三千年多年的历史。取材于棕榈树，制作简单，方便携带，且蒲扇的表我国已有三千年多年的历史。取材于棕榈树，制作简单，方便携带，且蒲扇的表面光滑，因而，古人常会在上面作画。古有棕扇、葵扇、蒲扇、蕉扇诸名，实即面光滑，因而，古人常会在上面作画。古有棕扇、葵扇、蒲扇、蕉扇诸名，实即今日的蒲扇，江浙称之为芭蕉扇。六七十年代，人们最常用的就是这种，似圆非今日的蒲扇，江浙称之为芭蕉扇。六七十年代，人们最常用的就是这种，似圆非圆，轻巧又便宜的蒲扇。蒲扇流传至今，我的记忆中，它跨越了半个世纪，圆，轻巧又便宜的蒲扇。蒲扇流传至今，我的记忆中，它跨越了半个世纪，也走过了我们的半个人

4、生的轨迹，携带着特有的念想，一年年，一天天，流向长也走过了我们的半个人生的轨迹，携带着特有的念想，一年年，一天天，流向长长的时间隧道，袅长的时间隧道，袅契约式设计摘要引言Eiffel 的 DbC 机制DbC与继承如何应用DbC2023/4/282Institute of Computer SoftwareNanjing Universitydeferred class PLANE inheritAIRCRAFTfeaturestart_take_off is-Initiate take-off procedures.requirecontrols.passedassigned_runway.c

5、leardeferredensureassigned_runway.owner=Currentmovingendstart_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.Postcondition20

6、23/4/289Institute of Computer SoftwareNanjing Universitydeferred 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=(

7、gauge=0.97*maximum)and(gauge 5 n:=n+9 n 13Most 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/4/2815Institute of C

8、omputer SoftwareNanjing UniversitySoftware correctnessConsider 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 TrueStrongest precond.Weakest postcond.“We are looking for someone whose work wil

9、l be to start from initial situations as characterized by P,and deliver results as defined by Q2023/4/2816Institute of Computer SoftwareNanjing University摘要引言Eiffel 的的 DbC 机制机制DbC与继承如何应用DbC2023/4/2817Institute of Computer SoftwareNanjing UniversityDesign by Contract:The MechanismPreconditions and Po

10、stconditionsClass InvariantRun-time effect2023/4/2818Institute of Computer SoftwareNanjing UniversityA contract(from EiffelBase)extend(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)=newkey_present:

11、has(key)inserted:insertedone_more:count=old count+12023/4/2819Institute of Computer SoftwareNanjing UniversityThe contractClientSupplierPRECONDITIONPOSTCONDITIONOBLIGATIONSPOSTCONDITIONPRECONDITIONBENEFITSRoutine2023/4/2820Institute of Computer SoftwareNanjing UniversityA class without contractsclas

12、s ACCOUNT feature-Accessbalance:INTEGER-BalanceMinimum_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/4/2821Institute of Computer SoftwareNanjing UniversityWithout c

13、ontracts(contd)feature-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:=(balance-sum=Min

14、imum_balance)endend2023/4/2822Institute of Computer SoftwareNanjing UniversityIntroducing contractsclassclass ACCOUNT createcreatemakefeaturefeature NONE-Initializationmake(initial_amount:INTEGER)is is-Set up account with initial_amount.requirerequirelarge_enough:initial_amount=Minimum_balancedodoba

15、lance:=initial_amountensureensurebalance_set:balance=initial_amountendend2023/4/2823Institute of Computer SoftwareNanjing UniversityIntroducing contracts(contd)feature-Accessbalance:INTEGER-BalanceMinimum_balance:INTEGER is 1000-Minimum balancefeature NONE-Implementation of deposit and withdrawaladd

16、(sum:INTEGER)is-Add sum to the balance(secret procedure).dobalance:=balance+sumensureincreased:balance=old balance+sum end2023/4/2824Institute of Computer SoftwareNanjing UniversityWith contracts(contd)feature-Deposit and withdrawal operations deposit(sum:INTEGER)is-Deposit sum into the account.requ

17、irenot_too_small:sum=0doadd(sum)ensureincreased:balance=old balance+sumend2023/4/2825Institute of Computer SoftwareNanjing UniversityWith contracts(contd)withdraw(sum:INTEGER)is-Withdraw sum from the account.requirenot_too_small:sum=0not_too_big:sum=Minimum_balance)endinvariantnot_under_minimum:bala

18、nce=Minimum_balanceend2023/4/2829Institute of Computer SoftwareNanjing UniversityThe 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/4/2830Institute of Computer

19、 SoftwareNanjing UniversityThe correctness of 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

20、the invariant of its own class.a.f()a.g()a.f()create a.make()S1S2S3S42023/4/2831Institute of Computer SoftwareNanjing UniversityExamplebalance=deposits.total withdrawals.totaldepositswithdrawalsbalancedepositswithdrawals(A1)(A2)2023/4/2832Institute of Computer SoftwareNanjing UniversityA more sophis

21、ticated versionclass 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_LIST2023/4/2833Institute of Computer SoftwareNanjing Univ

22、ersityNew version(contd)feature NONE-Initializationmake(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

23、:INTEGER-BalanceMinimum_balance:INTEGER is 1000-Minimum balance2023/4/2834New 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+su

24、mend2023/4/2835Institute of Computer SoftwareNanjing UniversityNew version(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_balanceconsistent:balance=deposits.total withdrawals.totalend

25、2023/4/2837Institute of Computer SoftwareNanjing UniversityThe correctness of a classFor every creation procedure cp:precp docp postcp and INVFor every exported routine r:INV and prer dor postr and INVa.f()a.g()a.f()create a.make()S1S2S3S42023/4/2838Institute of Computer SoftwareNanjing UniversityIn

26、itial versionfeaturefeature 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:balance=initial_amo

27、unt end end2023/4/2839Institute of Computer SoftwareNanjing UniversityCorrect versionfeaturefeature NONE-Initializationmake(initial_amount:INTEGER)is is-Set up account with initial_amount.requirerequirelarge_enough:initial_amount=Minimum_balancedodocreatecreate deposits.makecreatecreate withdrawals.

28、makedeposit(initial_amount)ensureensurebalance_set:balance=initial_amountendend402023/4/2840Institute of Computer SoftwareNanjing UniversityContracts:run-time effectCompilation options(per class,in Eiffel):No assertion checking Preconditions only Preconditions and postconditions Preconditions,postco

29、nditions,class invariants All assertions412023/4/2841Institute of Computer SoftwareNanjing University摘要引言Eiffel 的 DbC 机制DbC与继承与继承如何应用DbC2023/4/2842Institute of Computer SoftwareNanjing University继承与 Design by Contract问题：子类中的断言与父类中的断言是什么关系？依据子类乃父类的特化，子类的实例也是父类的合法实例。申明为父类的引用运行时可能指向子类实例因而？2023/4/2843In

30、stitute of Computer SoftwareNanjing UniversityInheritance and assertionsCorrect call:if a1.thena1.r(.)else.endr isensurer isensureCABa1:Aa1.r()2023/4/2844Institute of Computer SoftwareNanjing UniversityContractClientSupplier(Satisfy precondition:)不得要求投递超过5kg的包裹(Satisfy postcondition:)在3个工作日内投送到位OBLI

31、GATIONS(From postcondition:)3个工作日内包裹到位(From precondition:)不受理超过5kg的包裹BENEFITSdelivery2023/4/2845Institute of Computer SoftwareNanjing UniversityContractclass COURIER feature deliver(p:Package,d:Destination)require -包裹重量不超过5kg ensure -3个工作日内投送到指定地点 end2023/4/2846Institute of Computer SoftwareNanjing

32、UniversityMore desirable contractClientSupplier(Satisfy precondition:)不得要求投递超过8kg的包裹(Satisfy postcondition:)在2个工作日内投送到位OBLIGATIONS(From postcondition:)2个工作日内包裹到位(From precondition:)不受理超过8kg的包裹BENEFITSdelivery2023/4/2847Institute of Computer SoftwareNanjing UniversityMore desirable contractclass DIFF

33、ERENT_COURIERInherit COURIERredefine deliver feature deliver(p:Package,d:Destination)require -包裹重量不超过5kg require else -包裹重量不超过8kg ensure -3天内投送到指定地点 ensure then -2天内投送到指定地点 endrequire -包裹重量不超过8kgensure -2天内投送到指定地点2023/4/2848Institute of Computer SoftwareNanjing UniversityAssertion redeclaration rule

34、Redefined version may not have require or ensure.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/4/2849Institute of Computer SoftwareNanjing UniversityInvariant acc

35、umulationEvery class inherits all the invariant clauses of its parents.These clauses are conceptually“and”-ed.2023/4/2850Institute of Computer SoftwareNanjing University简言之可以使用require else削弱先验条件可以使用ensure then加强后验条件用and把不变式子句和你所继承的不变式子句结合起来，就可以加强不变式2023/4/2851Institute of Computer SoftwareNanjing Un

36、iversity摘要引言Eiffel 的 DbC 机制DbC与继承如何应用如何应用DbC其它 2023/4/2852Institute of Computer SoftwareNanjing UniversityDesign by Contract:How to apply目的：构造高质量的程序理解Contract violationDbC与Quality Assurance（QA）Precondition DesignNot defensive programmingClass Invariants and business logic2023/4/2853Institute of Comp

37、uter SoftwareNanjing UniversityWhat 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,debug

38、ging(especially in connection with the use of libraries).Exception handling.2023/4/2854Institute of Computer SoftwareNanjing UniversitySome benefits:technicalDevelopment process becomes more focused.Writing to spec.Sound basis for writing reusable software.Exception handling guided by precise defini

39、tion 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.2023/4/2855Institute of Computer SoftwareNanjing UniversitySome ben

40、efits: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 betwee

41、n all actors of the process:developers,managers,potentially customers.Component-based development possible on a solid basis.2023/4/2856Institute of Computer SoftwareNanjing UniversityA contract violation is not a special caseFor special cases(e.g.“if the sum is negative,report an error.”)use standar

42、d control structures(e.g.if.then.else.).A run-time assertion violation is something else:the manifestation ofA DEFECT(“BUG”)2023/4/2857Institute of Computer SoftwareNanjing UniversityContracts and quality assurancePrecondition violation:Bug in the client.Postcondition violation:Bug in the supplier.I

43、nvariant violation:Bug in the supplier.P A Q2023/4/2858Institute of Computer SoftwareNanjing UniversityContracts and bug typesPreconditions are particularly useful to find bugs in client code:YOUR APPLICATIONCOMPONENT LIBRARYyour_list.insert(y,a+b+1)i=0class LIST G2023/4/2859Institute of Computer So

44、ftwareNanjing UniversityContracts 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 assertions2023/4/

45、2860Institute of Computer SoftwareNanjing UniversityContracts 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

46、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 Ma

47、rco,IEEE Computer,19972023/4/2861Institute of Computer SoftwareNanjing UniversityContract 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-mon

48、itoring version ready for shipping.Result of an assertion violation:exception.Ideally:static checking(proofs)rather than dynamic monitoring.2023/4/2862Institute of Computer SoftwareNanjing UniversityContracts and documentation契约能使文档更出色更清晰的文档契约乃是类特性的公开视图中的固有成分更可靠的文档运行时要检查断言，以便保证制定的契约与程序的实际运行情况一致明确的测试

49、指导断言定义了测试的预期结果，并且由代码进行维护更精确的规范既能够获得精确规范得到的益处，同时还使得程序员继续以他们所熟悉的方式工作2023/4/2863Institute of Computer SoftwareNanjing UniversityContract form:DefinitionSimplified form of class text,retaining interface elements only:Remove any non-exported(private)feature.For the exported(public)features:Remove body(do

50、 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?)2023/4/2864Institute of Computer SoftwareNanjing UniversityContract form of ACCOUNT classclass interfa