最病 A Contracts for analysis (cont'd) fill OBLIGATIONS BENEFITS Client (Satisfy precondition: (From postcondition Make sure input valve Get filled-up vat, with is open output valve is both valves closed closed Supplier (Satisfy postcondition: )(From precondition Fill the vat and close Simpler processing both valves thanks to assumption that valves are in the proper initial position Institute of Computer Software 2021/1/30 Nanjing UniversityContracts for analysis (cont’d) 2021/1/30 Institute of Computer Software Nanjing University 11 Client Supplier (Satisfy precondition:) Make sure input valve is open, output valve is closed. (Satisfy postcondition:) Fill the vat and close both valves. OBLIGATIONS (From postcondition:) Get filled-up vat, with both valves closed. (From precondition:) Simpler processing thanks to assumption that valves are in the proper initial position. BENEFITS fill