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 University2021/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