&雪扇 Contracts for analysis(cont'd) 102 11 f训 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 2022-2-27 Nanjing University
Contracts for analysis (cont’d) 2022-2-27 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
&扇 So,is it like "assert,h"? 12 (Source:Reto Kramer) Design by Contract goes further: ▣“Assert'”does not provide a contract. Clients cannot see asserts as part of the interface. Asserts do not have associated semantic specifications. Not explicit whether an assert represents a precondition, post-conditions or invariant. Asserts do not support inheritance. Asserts do not yield automatic documentation. Institute of Computer Software 2022-2-27 Nanjing University
So, is it like “assert.h”? (Source: Reto Kramer) Design by Contract goes further: “Assert” does not provide a contract. Clients cannot see asserts as part of the interface. Asserts do not have associated semantic specifications. Not explicit whether an assert represents a precondition, post-conditions or invariant. Asserts do not support inheritance. Asserts do not yield automatic documentation. 2022-2-27 Institute of Computer Software Nanjing University 12
Contracts 1902 13 契约就是“规范和检查”！ Precondition:针对method,它规定了在调用该方法 之前必须为真的条件 口Postcondition:针对method,它规定了方法顺利执行 完毕之后必须为真的条件 Invariant:针对整个类，它规定了该类任何实例调 用任何方法都必须为真的条件 Institute of Computer Software 2022-2-27 Nanjing University
Contracts 契约就是“规范和检查”！ Precondition：针对method，它规定了在调用该方法 之前必须为真的条件 Postcondition：针对method，它规定了方法顺利执行 完毕之后必须为真的条件 Invariant：针对整个类，它规定了该类任何实例调 用任何方法都必须为真的条件 2022-2-27 Institute of Computer Software Nanjing University 13
Correctness in software 102 UNIVE 14 Correctness is a relative notion:consistency of implementation vis-a-vis specification.(This assumes there is a specification!) Basic notation:(P,Q:assertions,i.e.properties of the state of the computation.A:instructions). IP)A (Q) "Hoare triple" What this means(total correctness): Any execution of A started in a state satisfying P will terminate in a state satisfying Q. Institute of Computer Software 2022-2-27 Nanjing University
Correctness in software Correctness is a relative notion: consistency of implementation vis-a-vis specification. (This assumes there is a specification!) Basic notation: (P, Q: assertions, i.e. properties of the state of the computation. A: instructions). {P} A {Q} “Hoare triple ” What this means (total correctness): Any execution of A started in a state satisfying P will terminate in a state satisfying Q. 2022-2-27 Institute of Computer Software Nanjing University 14
&扇 Hoare triples:a simple example 102 15 {n>5}n:=n+9{n>13} Most interesting properties: Strongest postcondition(from given precondition). Weakest precondition(from given postcondition). P is stronger than or equal to Q"means: P implies Q QUIZ:What is the strongest possible assertion?The weakest? Institute of Computer Software 2022-2-27 Nanjing University
Hoare triples: a simple example {n > 5} n := n + 9 {n > 13} Most interesting properties: Strongest postcondition (from given precondition). Weakest precondition (from given postcondition). “P is stronger than or equal to Q” means: P implies Q QUIZ: What is the strongest possible assertion? The weakest? 2022-2-27 Institute of Computer Software Nanjing University 15