Design by Contract 契约式设计 Institute of Computer Software 2022-2-27 Nanjing University
契约式设计 Design by Contract 2022-2-27 Institute of Computer Software Nanjing University
&雪扇 摘要 UNIVE 2 口引言 o Eiffel的DbC机制 口DbC与继承 口如何应用DbC Institute of Computer Software 2022-2-27 Nanjing University
摘要 引言 Eiffel 的 DbC 机制 DbC与继承 如何应用DbC 2022-2-27 Institute of Computer Software Nanjing University 2
引言 1902 3 口Design by Contract(DbC)契约式设计 口方法学层面的思想 ■以尽可能小的代价开发出可靠性出众的软件系统 Eiffel语言的直接支持 Bertrand Meyer:DbC是构建面向对象软件系统方法 O 的核心！ 口James McKim:“只要你会写程序，你就会写契约” Institute of Computer Software 2022-2-27 Nanjing University
引言 Design by Contract (DbC) 契约式设计 方法学层面的思想 以尽可能小的代价开发出可靠性出众的软件系统 Eiffel语言的直接支持 Bertrand Meyer：DbC是构建面向对象软件系统方法 的核心！ James McKim： “只要你会写程序，你就会写契约” 2022-2-27 Institute of Computer Software Nanjing University 3
引言 1902 4 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. (把类和它的客户程序之间的关系看做正式的协议，描 述双方的权利和义务) Institute of Computer Software 2022-2-27 Nanjing University
引言 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. （把类和它的客户程序之间的关系看做正式的协议，描 述双方的权利和义务） 2022-2-27 Institute of Computer Software Nanjing University 4
&扇 NAN 引言 1902 5 o 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. Institute of Computer Software 2022-2-27 Nanjing University
引言 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. 2022-2-27 Institute of Computer Software Nanjing University 5
&雪扇 A human contract 102 UNIVE 6 deliver OBLIGATIONS(义务) BENEFITS(权益/权利) Client (Satisfy precondition: (From postcondition: Bring package before Get package delivered 4 p.m.;pay fee. by 10 a.m.next day. (Satisfy postcondition: (From precondition: Supplier Deliver package by Not required to do 10 a.m.next day. anything if package delivered after 4 p.m., or fee not paid. Institute of Computer Software 2022-2-27 Nanjing University
A human contract 2022-2-27 Institute of Computer Software Nanjing University 6 Client Supplier (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. BENEFITS(权益/权利) deliver
&扇 NAN A view of software construction UNIVE ▣ Constructing 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. Institute of Computer Software 2022-2-27 Nanjing University
A view of software construction Constructing 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. 2022-2-27 Institute of Computer Software Nanjing University 7
Properties of contracts 102 8 ▣A 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). Institute of Computer Software 2022-2-27 Nanjing University
Properties of contracts A 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). 2022-2-27 Institute of Computer Software Nanjing University 8
Contracts for analysis deferred class PLANE inherit AIRCRAFT feature start_take_off is Precondition --Initiate take-off procedures. require controls.passed --i.e.specified only. assigned_runway.clear deferred --not implemented. ensure assigned_runway.owner Current moving Postcondition end start_landing,increase_altitude,decrease_altitude,moving, altitude,speed,time_since_take_off .[Other features]… Class invariant invariant (time_since_take_off <=20)implies (assigned_runway.owner Current) moving =(speed 10) 9 end Institute of Computer Software 2022-2-27 Nanjing University
2022-2-27 Institute of Computer Software Nanjing University 9 deferred 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 10) end Contracts for analysis Precondition Class invariant -- i.e. specified only. -- not implemented. Postcondition
Contracts for analysis(cont'd) deferred class VAT inherit TANK feature in_valve,out_valve:VALVE fill is -Fill the vat. Precondition require in_valve.open out_valve.closed --i.e.specified only. deferred ensure --not implemented. in_valve.closed out_valve.closed is full Postcondition end empty,is_full,is_empty,gauge,maximum,...[Other features]... Class invariant invariant is_full =(gauge >=0.97 maximum)and (gauge <=1.03 maximum) end 10 Institute of Computer Software 2022-2-27 Nanjing University
2022-2-27 Institute of Computer Software Nanjing University 10 deferred 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) end Contracts for analysis (cont’d) Precondition Class invariant -- i.e. specified only. -- not implemented. Postcondition