《契约式设计》PPT课件.ppt

《《契约式设计》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《契约式设计》PPT课件.ppt（85页珍藏版）》请在三一办公上搜索。

1、契约式设计,Design by Contract,2023/8/4,Institute of Computer SoftwareNanjing University,摘要,引言Eiffel 的 DbC 机制DbC与继承如何应用DbC,2023/8/4,Institute of Computer SoftwareNanjing University,2,引言,Design by Contract(DbC)契约式设计方法学层面的思想以尽可能小的代价开发出可靠性出众的软件系统Eiffel语言的直接支持Bertrand Meyer：DbC是构建面向对象软件系统方法的核心！James McKim：“只要

2、你会写程序，你就会写契约”,2023/8/4,Institute of Computer SoftwareNanjing University,3,引言,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/8/4,Institute of Computer SoftwareNanjing University,4,引言,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 el

4、ement should beExplicit.Part of the software element itself.,2023/8/4,Institute of Computer SoftwareNanjing University,5,A human contract,2023/8/4,Institute of Computer SoftwareNanjing University,6,Client,Supplier,(Satisfy precondition:)Bring package before 4 p.m.;pay fee.,(Satisfy postcondition:)De

5、liver 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.,BENEFITS(权益/权利),deliver,A view of software construction,Constructing systems as structur

6、ed collections of cooperating software elements suppliers and clients cooperating on the basis of clear definitions of obligations and benefits.These definitions are the contracts.,2023/8/4,Institute of Computer SoftwareNanjing University,7,Properties of contracts,A contract:Binds two parties(or mor

7、e):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 co

8、ntracts(laws,regulations,standard practices).,2023/8/4,Institute of Computer SoftwareNanjing University,8,2023/8/4,Institute of Computer SoftwareNanjing University,9,deferred class PLANE inheritAIRCRAFTfeaturestart_take_off is-Initiate take-off procedures.requirecontrols.passedassigned_runway.cleard

9、eferredensureassigned_runway.owner=Currentmovingendstart_landing,increase_altitude,decrease_altitude,moving,altitude,speed,time_since_take_off.Other features.invariant(time_since_take_off 10)end,Contracts for analysis,2023/8/4,Institute of Computer SoftwareNanjing University,10,deferred class VAT in

10、heritTANKfeaturein_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=1.03*maximum)end,Contracts for analysis(contd),C

11、ontracts for analysis(contd),2023/8/4,Institute of Computer SoftwareNanjing University,11,Client,Supplier,(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 b

12、oth valves closed.,(From precondition:)Simpler processing thanks to assumption that valves are in the proper initial position.,BENEFITS,fill,So,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 inte

13、rface.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.,2023/8/4,Institute of Computer SoftwareNanjing University,12,Contracts,契

14、约就是“规范和检查”！Precondition：针对method，它规定了在调用该方法之前必须为真的条件Postcondition：针对method，它规定了方法顺利执行完毕之后必须为真的条件Invariant：针对整个类，它规定了该类任何实例调用任何方法都必须为真的条件,2023/8/4,Institute of Computer SoftwareNanjing University,13,Correctness in software,Correctness is a relative notion:consistency of implementation vis-a-vis speci

15、fication.(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.,2023/8/4,Ins

16、titute of Computer SoftwareNanjing University,14,Hoare triples:a simple example,n 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 pos

17、sible assertion?The weakest?,2023/8/4,Institute of Computer SoftwareNanjing University,15,Software correctness,Consider 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 True,2023/8/4,Institute o

18、f Computer SoftwareNanjing University,16,Strongest precond.,Weakest postcond.,“We are looking for someone whose work will be to start from initial situations as characterized by P,and deliver results as defined by Q,摘要,引言Eiffel 的 DbC 机制DbC与继承如何应用DbC,2023/8/4,Institute of Computer SoftwareNanjing Uni

19、versity,17,Design by Contract:The Mechanism,Preconditions and PostconditionsClass InvariantRun-time effect,2023/8/4,Institute of Computer SoftwareNanjing University,18,A contract(from EiffelBase),2023/8/4,Institute of Computer SoftwareNanjing University,19,extend(new:G;key:H)-Assuming there is no it

20、em of key key,-insert new with key;set inserted.requirekey_not_present:not has(key)ensureinsertion_done:item(key)=newkey_present:has(key)inserted:insertedone_more:count=old count+1,The contract,2023/8/4,Institute of Computer SoftwareNanjing University,20,Client,Supplier,PRECONDITION,POSTCONDITION,OB

21、LIGATIONS,POSTCONDITION,PRECONDITION,BENEFITS,Routine,A class without contracts,class 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

22、:=balance+sumend,2023/8/4,Institute of Computer SoftwareNanjing University,21,Without contracts(contd),2023/8/4,Institute of Computer SoftwareNanjing University,22,feature-Deposit and withdrawal operationsdeposit(sum:INTEGER)is-Deposit sum into the account.doadd(sum)endwithdraw(sum:INTEGER)is-Withdr

23、aw sum from the account.doadd(sum)endmay_withdraw(sum:INTEGER):BOOLEAN is-Is it permitted to withdraw sum from the account?doResult:=(balance-sum=Minimum_balance)endend,Introducing contracts,class ACCOUNT createmakefeature NONE-Initializationmake(initial_amount:INTEGER)is-Set up account with initial

24、_amount.requirelarge_enough:initial_amount=Minimum_balancedobalance:=initial_amountensurebalance_set:balance=initial_amountend,2023/8/4,Institute of Computer SoftwareNanjing University,23,Introducing contracts(contd),2023/8/4,Institute of Computer SoftwareNanjing University,24,feature-Accessbalance:

25、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+sumensureincreased:balance=old balance+sum end,With contracts(contd),2023/8/4,Institute of Computer Softwa

26、reNanjing University,25,feature-Deposit and withdrawal operationsdeposit(sum:INTEGER)is-Deposit sum into the account.requirenot_too_small:sum=0doadd(sum)ensureincreased:balance=old balance+sumend,With contracts(contd),withdraw(sum:INTEGER)is-Withdraw sum from the account.requirenot_too_small:sum=0no

27、t_too_big:sum=balance Minimum_balancedoadd(sum)-i.e.balance:=balance sumensuredecreased:balance=old balance-sumend,2023/8/4,Institute of Computer SoftwareNanjing University,26,The contract,2023/8/4,Institute of Computer SoftwareNanjing University,27,Client,Supplier,(Satisfy precondition:)Make sure s

28、um 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.,BENEFITS,withdraw,The imperative and the appli

29、cative,2023/8/4,Institute of Computer SoftwareNanjing University,28,dobalance:=balance-sum,ensurebalance=old balance-sum,PRESCRIPTIVE,DESCRIPTIVE,How?,Operational,Implementation,Command,Instruction,Imperative,What?,Denotational,Specification,Query,Expression,Applicative,With contracts(end),may_withd

30、raw(sum:INTEGER):BOOLEAN is-Is it permitted to withdraw sum from the-account?doResult:=(balance-sum=Minimum_balance)endinvariantnot_under_minimum:balance=Minimum_balanceend,2023/8/4,Institute of Computer SoftwareNanjing University,29,The class invariant,Consistency constraint applicable to all insta

31、nces of a class.Must be satisfied:After creation.After execution of any feature by any client.(Qualified calls only:a.f(.),2023/8/4,Institute of Computer SoftwareNanjing University,30,The correctness of a class,For every creation procedure cp:precp docp postcp and INVFor every exported routine r:INV

32、 and prer dor postr and INVThe 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/8/4,Institute of Computer SoftwareNanjing University,31,Example,balance=deposits.total withdrawals.total,2

33、023/8/4,Institute of Computer SoftwareNanjing University,32,deposits,withdrawals,balance,deposits,withdrawals,(A1),(A2),A more sophisticated version,2023/8/4,Institute of Computer SoftwareNanjing University,33,class ACCOUNT createmakefeature NONE-Implementationadd(sum:INTEGER)is-Add sum to the balan

34、ce(secret procedure).dobalance:=balance+sumensurebalance_increased:balance=old balance+sum enddeposits:DEPOSIT_LISTwithdrawals:WITHDRAWAL_LIST,New version(contd),feature NONE-Initializationmake(initial_amount:INTEGER)is-Set up account with initial_amount.requirelarge_enough:initial_amount=Minimum_ba

35、lancedo balance:=initial_amountcreate deposits.makecreate withdrawals.makeensurebalance_set:balance=initial_amountendfeature-Accessbalance:INTEGER-BalanceMinimum_balance:INTEGER is 1000-Minimum balance,2023/8/4,34,New version(contd),feature-Deposit and withdrawal operationsdeposit(sum:INTEGER)is-Dep

36、osit sum into the account.requirenot_too_small:sum=0doadd(sum)deposits.extend(create DEPOSIT.make(sum)ensureincreased:balance=old balance+sumend,2023/8/4,Institute of Computer SoftwareNanjing University,35,New version(contd),2023/8/4,Institute of Computer SoftwareNanjing University,36,withdraw(sum:I

37、NTEGER)is-Withdraw sum from the account.requirenot_too_small:sum=0not_too_big:sum=balance Minimum_balancedo add(sum)withdrawals.extend(create WITHDRAWAL.make(sum)ensure decreased:balance=old balance sum one_more:withdrawals.count=old withdrawals.count+1end,New version(end),2023/8/4,Institute of Comp

38、uter SoftwareNanjing University,37,may_withdraw(sum:INTEGER):BOOLEAN is-Is it permitted to withdraw sum from the-account?doResult:=(balance-sum=Minimum_balance)endinvariantnot_under_minimum:balance=Minimum_balanceconsistent:balance=deposits.total withdrawals.totalend,The correctness of a class,For e

39、very creation procedure cp:precp docp postcp and INVFor every exported routine r:INV and prer dor postr and INV,2023/8/4,Institute of Computer SoftwareNanjing University,38,a.f(),a.g(),a.f(),create a.make(),S1,S2,S3,S4,Initial version,2023/8/4,Institute of Computer SoftwareNanjing University,39,feat

40、ure NONE-Initializationmake(initial_amount:INTEGER)is-Set up account with initial_amount.require large_enough:initial_amount=Minimum_balancedobalance:=initial_amount create deposits.makecreate withdrawals.makeensurebalance_set:balance=initial_amount end,Correct version,2023/8/4,Institute of Computer

41、 SoftwareNanjing University,40,feature NONE-Initializationmake(initial_amount:INTEGER)is-Set up account with initial_amount.requirelarge_enough:initial_amount=Minimum_balancedocreate deposits.makecreate withdrawals.makedeposit(initial_amount)ensurebalance_set:balance=initial_amountend,40,Contracts:r

42、un-time effect,Compilation options(per class,in Eiffel):No assertion checking Preconditions only Preconditions and postconditions Preconditions,postconditions,class invariants All assertions,2023/8/4,Institute of Computer SoftwareNanjing University,41,41,摘要,引言Eiffel 的 DbC 机制DbC与继承如何应用DbC,2023/8/4,In

43、stitute of Computer SoftwareNanjing University,42,继承与 Design by Contract,问题：子类中的断言与父类中的断言是什么关系？依据子类乃父类的特化，子类的实例也是父类的合法实例。申明为父类的引用运行时可能指向子类实例因而？,2023/8/4,Institute of Computer SoftwareNanjing University,43,Inheritance and assertions,2023/8/4,Institute of Computer SoftwareNanjing University,44,Correct

44、 call:if a1.thena1.r(.)else.end,r is,ensure,r is,ensure,C,A,B,a1:A,a1.r(),Contract,2023/8/4,Institute of Computer SoftwareNanjing University,45,Client,Supplier,(Satisfy precondition:)不得要求投递超过5kg的包裹,(Satisfy postcondition:)在3个工作日内投送到位,OBLIGATIONS,(From postcondition:)3个工作日内包裹到位,(From precondition:)不受

45、理超过5kg的包裹,BENEFITS,delivery,Contract,class COURIER feature deliver(p:Package,d:Destination)require-包裹重量不超过5kg ensure-3个工作日内投送到指定地点 end,2023/8/4,Institute of Computer SoftwareNanjing University,46,More desirable contract,2023/8/4,Institute of Computer SoftwareNanjing University,47,Client,Supplier,(Sa

46、tisfy precondition:)不得要求投递超过8kg的包裹,(Satisfy postcondition:)在2个工作日内投送到位,OBLIGATIONS,(From postcondition:)2个工作日内包裹到位,(From precondition:)不受理超过8kg的包裹,BENEFITS,delivery,More desirable contract,class DIFFERENT_COURIERInherit COURIERredefine deliver feature deliver(p:Package,d:Destination)require-包裹重量不超过5

47、kg require else-包裹重量不超过8kg ensure-3天内投送到指定地点 ensure then-2天内投送到指定地点 end,2023/8/4,Institute of Computer SoftwareNanjing University,48,require-包裹重量不超过8kg,ensure-2天内投送到指定地点,Assertion redeclaration rule,Redefined version may not have require or ensure.May have nothing(assertions kept by default),orrequi

48、re else new_preensure then new_postResulting assertions are:original_precondition or new_preoriginal_postcondition and new_post,2023/8/4,Institute of Computer SoftwareNanjing University,49,Invariant accumulation,Every class inherits all the invariant clauses of its parents.These clauses are conceptu

49、ally“and”-ed.,2023/8/4,Institute of Computer SoftwareNanjing University,50,简言之,可以使用require else削弱先验条件可以使用ensure then加强后验条件用and把不变式子句和你所继承的不变式子句结合起来，就可以加强不变式,2023/8/4,Institute of Computer SoftwareNanjing University,51,摘要,引言Eiffel 的 DbC 机制DbC与继承如何应用DbC其它,2023/8/4,Institute of Computer SoftwareNanjing

50、 University,52,Design by Contract:How to apply,目的：构造高质量的程序理解Contract violationDbC与Quality Assurance（QA）Precondition DesignNot defensive programmingClass Invariants and business logic,2023/8/4,Institute of Computer SoftwareNanjing University,53,What are contracts good for?,Writing correct software(an