tailieunhanh - Lecture Formal methods in software engineering - Lecture 26

In this chapter, the following content will be discussed: Conditional correctness, weakest pre-condition, broad CAT of statements, assignment axiom, rules for sequential composition, rules for conditional,. | 1 1 Formal Methods in Software Engineering Lecture # 26 1 1 1 2 2 Conditional Correctness { P} S {Q} (initial state) (set of instruction) (Final State) Expresses the conditional correctness of S Binary search (pre-condition) - > Array must be in sorted form Which means that, in-order to work this program properly we need to start with a given condition. Post Condition: If the key is present then you will get the index, if the key is not present then you will get some value which will tell you that the key is not present (desired output). If we start with “P” and ended with “Q” then our program is conditional corret. 2 2 2 3 3 Conditional Correctness Suppose : post condition: n e represents an expression X will have the value which e had before executing the statement Q(e) denotes the predicate obtained by substituting e for all free occurrences of x in the predicate Q 7 7 7 8 8 Assignment Axiom Wp (i : = i-1, i = 0 ) i -1 = 0 Wp | 1 1 Formal Methods in Software Engineering Lecture # 26 1 1 1 2 2 Conditional Correctness { P} S {Q} (initial state) (set of instruction) (Final State) Expresses the conditional correctness of S Binary search (pre-condition) - > Array must be in sorted form Which means that, in-order to work this program properly we need to start with a given condition. Post Condition: If the key is present then you will get the index, if the key is not present then you will get some value which will tell you that the key is not present (desired output). If we start with “P” and ended with “Q” then our program is conditional corret. 2 2 2 3 3 Conditional Correctness Suppose : post condition: n <0 S: n = n-1 Pre-condition: We started with n=0; n-1; end: n-1 Another point: We started with n = -10 ; n-1; -11 Which means that there are infinite number of values for n which will satisfy the post condition. Weakest Pre-condition: N <= 0 (infinite possibilities ) and then – then get n <0 3 3 3 4 4 Weakest .