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