Software correctness 102 16 "We are looking for someone Consider whose work will be to start from initial situations as characterized by P,and deliver (P)A (Q) results as defined by 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: Strongest precond. ▣1.{False}A{ 口2.{}A{True} Weakest postcond. Institute of Computer Software 2022-2-27 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} 2022-2-27 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
&雪扇 摘要 UNIVE 17 口引言 o Eiffel的DbC机制 口DbC与继承 口如何应用DbC Institute of Computer Software 2022-2-27 Nanjing University
摘要 引言 Eiffel 的 DbC 机制 DbC与继承 如何应用DbC 2022-2-27 Institute of Computer Software Nanjing University 17
&扇 Design by Contract:The Mechanism 1002 UNIVE 18 Preconditions and Postconditions Class Invariant Run-time effect Institute of Computer Software 2022-2-27 Nanjing University
Design by Contract: The Mechanism Preconditions and Postconditions Class Invariant Run-time effect 2022-2-27 Institute of Computer Software Nanjing University 18
&扇 A contract(from EiffelBase) 102 UNIVE 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 Institute of Computer Software 2022-2-27 Nanjing University
A contract (from EiffelBase) 2022-2-27 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
条 The contract UNIVER 20 Routine OBLIGATIONS BENEFITS Client PRECONDITION POSTCONDITION Supplier POSTCONDITION PRECONDITION Institute of Computer Software 2022-2-27 Nanjing University
The contract 2022-2-27 Institute of Computer Software Nanjing University 20 Client Supplier PRECONDITION POSTCONDITION OBLIGATIONS POSTCONDITION PRECONDITION BENEFITS Routine