最病 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 UniversityCorrectness 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