最病 o Software correctness We are looking for someone 口 Consider whose work will be to start from initial situations as characterized by p, and deli PPJAQH results as defined by Q a Take this as a job ad in the classifieds. a Should a lazy employment candidate hope for a weak or strong p What about Q Strongest precond o wo special offers 口1.{Fase}A 口2.{-}A{True Weakest postcond Institute of Computer Software 2021/1/30 Nanjing University
Software correctness Consider {P} A {Q} Take this as a job ad in the classifieds. Should a lazy employment candidate hope for a weak or strong P? What about Q? Two special offers: 1. {False} A {...} 2. {...} A {True} 2021/1/30 Institute of Computer Software Nanjing University 16 Strongest precond. Weakest postcond. “We are looking for someone whose work will be to start from initial situations as characterized by P, and deliver results as defined by Q
最病 过摘要 口引言 口Eife的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 17
最病 A Design by Contract: The Mechanism a Preconditions and postconditions 口C| ass Invariant 口RUn- ime effect Institute of Computer Software 2021/1/30 Nanjing University
Design by Contract: The Mechanism Preconditions and Postconditions Class Invariant Run-time effect 2021/1/30 Institute of Computer Software Nanjing University 18
最病 E A contract(from EiffelBase extend(new: G; key: H) insert new with key; set inserted, Assuming there is no item of key reqUire key_not_present: not has( key) ensure insertion_done: item(key) new key_present: has(key) inserted: inserted one more: count old count Institute of Computer Software 2021/1/30 Nanjing University
A contract (from EiffelBase) 2021/1/30 Institute of Computer Software Nanjing University 19 extend (new: G; key: H) -- Assuming there is no item of key key, -- insert new with key; set inserted. require key_not_present: not has (key) ensure insertion_done: item (key) = new key_present: has (key) inserted: inserted one_more: count = old count + 1
最病 A The contract Routine OBLIGATIONS BENEFITS Client PRECONDITION POSTCONDITION Supplier POSTCONDITION PRECONDITION Institute of Computer Software 2021/1/30 Nanjing University
The contract 2021/1/30 Institute of Computer Software Nanjing University 20 Client Supplier PRECONDITION POSTCONDITION OBLIGATIONS POSTCONDITION PRECONDITION BENEFITS Routine