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