最病 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 < 20)implies(assigned_runway. owner Current) ing =(speed> 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 <= 20) implies (assigned_runway.owner = Current) moving = (speed > 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