Design by Contract 契约式设计 Institute of Computer Software 2021/1/30 Nanjing University
契约式设计 Design by Contract 2021/1/30 Institute of Computer Software Nanjing University
最病 过摘要 2 口引言 口Efe的DbC机制 口DbC与继承 口如何应用DbC Institute of Computer Software 2021/1/30 Nanjing University
摘要 引言 Eiffel 的 DbC 机制 DbC与继承 如何应用DbC 2021/1/30 Institute of Computer Software Nanjing University 2
最病 以引言 口 Design by Contract(DbC)契约式设计 口方法学层面的思想 ■以尽可能小的代价开发出可靠性出众的软件系统 ■Eif语言的直接支持 口 Bertrand Meyer:DbC是构建面向对象软件系统方法 的核心! 口 James mckim:“只要你会写程序,你就会写契约 Institute of Computer Software 2021/1/30 Nanjing University
引言 Design by Contract (DbC) 契约式设计 方法学层面的思想 ◼ 以尽可能小的代价开发出可靠性出众的软件系统 ◼ Eiffel语言的直接支持 Bertrand Meyer：DbC是构建面向对象软件系统方法 的核心！ James McKim：“只要你会写程序，你就会写契约” 2021/1/30 Institute of Computer Software Nanjing University 3
最病 以引言 o a discipline of analysis, design, implementation, management (可以贯穿于软件创建的全过程,从分析到设计,从文 档到调试,甚至可以渗透到项目管理中) a Viewing the relationship between a class and its clients as a formal agreement, expressing each party s rights and obligations. (把类和它的客户程序之间的关系看做正式的协议,描 述双方的权利和义务) Institute of Computer Software 2021/1/30 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. （把类和它的客户程序之间的关系看做正式的协议，描 述双方的权利和义务） 2021/1/30 Institute of Computer Software Nanjing University 4
最病 以引言 5 n Every software element is intended to satisfy a certain goal, for the benefit of other software elements (and ultimately of human users) n This goal is the elements contract. a The contract of any software element should be 口 Explicit. a Part of the software element itself Institute of Computer Software 2021/1/30 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. 2021/1/30 Institute of Computer Software Nanjing University 5
最病 E Ahuman contract 6 deliver OBLIGATIONS(义务) BENEF|TS(权益/权利) Client Satisfy precondition: From postcondition Bring package before Get package delivered 4 p. m. pay fee by 10 a.m. next day Suppli \satisfy postcondition: (From precondition 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 2021/1/30 Nanjing University
A human contract 2021/1/30 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
最病 A view of software construction 7 n Constructing systems as structured collections of cooperating software elements- suppliers and clients- cooperating on the basis of clear definitions of obligations and benetits. a these definitions are the contracts Institute of Computer Software 2021/1/30 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. 2021/1/30 Institute of Computer Software Nanjing University 7
最病 A Properties of contracts 8 A contract a Binds two parties (or more): supplier, client. a Is explicit(written). a Specifies mutual obligations and benefits. a Usually maps obligation for one of the parties into benefit or the other, and conversely. a Has no hidden clauses: obligations are those specified a Often relies, implicitly or explicitly on general rules applicable to all contracts ( laws, regulations, standard practices Institute of Computer Software 2021/1/30 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). 2021/1/30 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 lot implemented assigned_runway. owner =Current moving Postcondition start_landing, increase_altitude, decrease_altitude, moving altitude speed, time_since_ take_ off …,[ Other features]… Class invariant invariant (timesince_ take_off 10) 9 d en Institute of Computer Software 2021/1/30 Nanjing University
2021/1/30 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 ut valve closed i.e. specified only deferred ensure in valve, closed not implemented out valvecl is full Postcondition empty, is_full, is_empty, gauge, maximum, [Other fe Class invariant invariant (gauge >=0.97*maximum) and (gauge <=1.03*maximum) end 10 Institute of Computer Software 2021/1/30 Nanjing University
2021/1/30 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