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 .

• Kỹ thuật lập trình
• Software engineering
• Formal methods in software engineering
• Software development methods
• Formal languages
• Automata theory
• Software verification
• Object oriented software engineering
• Practical software development
• Object orientation
• Software quality
• Software engineering projects
• Introduction to software engineering
• Lecture Introduction to software engineering
• Công nghệ phần mềm
• Software process
• Software engineering ethics
• Lecture Software engineering
• Professional software development
• Software process activities
• Software engineering diversity
• Introduction Software Engineering
• Software products
• FAQs about software engineering
• Essential attributes of good software
• Importance of software engineering
• Software processes
• Aspect oriented software engineering
• The separation of concerns
• Software engineering with aspects
• Quality concepts
• Detail Design
• Design Software Engineering
• Implementation Software Engineering
• Build Software Engineering
• Buy Software Engineering
• Requirement engineering
• Requirement engineering process
• Software requirements engineering
• Lecture Software requirements engineering
• Requirements engineering
• Software requirements engineering
• Lecture Software requirements engineering
• System engineering
• Software requirements document
• Requirements engineering process tasks