Lecture Formal methods in software engineering - Lecture 27 presents the following content: Conditional statements, invariant condition in iteration, loop invariants, weakest pre-condition for while statement,. | 1 1 Formal Methods in Software Engineering Lecture # 27 1 1 1 2 2 Classical Problem Can you completely cover the chessboard with these dominoes without partially using a domino? If so how. If not prove that you cannot. 2 2 2 3 3 Classical Problem Key of invariant condition . Shape of the tiles which we are using to cover the chessboard ( some information store in color) Given piece will cover one light and one blue tile because on a cheeseboard we do not have two white or black tiles adjusnt to each other We have equal number of blue and white squares on chessboard If do not have equal number of squares then we will not cover the whole chessboard Condition: We have removed two squares of the same color . We are left with more blue then white . 32 blue and 30 whites 3 3 3 4 4 Conditional statements If ( i j) m :=j ; (m = i or m = j) and ( m j) and ( j =i or j = j ) and ( j j ) and (true) and ( jj) and ( j j) 5 5 5 - (i > j) is a subset of (jj) Universal set 7 7 7 8 8 Tower of Hanoi 8 8 8 9 9 Tower of Hanoi 9 9 9 10 10 Tower of Hanoi 10 10 10 11 11 Invariant condition in Iteration Recursive solution is given in every book But we need to find iterative solution Odd number moves involved smallest disk Smallest disk move in clock-wise or anti-clock wise depending on the number of disks If you | 1 1 Formal Methods in Software Engineering Lecture # 27 1 1 1 2 2 Classical Problem Can you completely cover the chessboard with these dominoes without partially using a domino? If so how. If not prove that you cannot. 2 2 2 3 3 Classical Problem Key of invariant condition . Shape of the tiles which we are using to cover the chessboard ( some information store in color) Given piece will cover one light and one blue tile because on a cheeseboard we do not have two white or black tiles adjusnt to each other We have equal number of blue and white squares on chessboard If do not have equal number of squares then we will not cover the whole chessboard Condition: We have removed two squares of the same color . We are left with more blue then white . 32 blue and 30 whites 3 3 3 4 4 Conditional statements If ( i <= j ) then m : = i; else m :=j (m <= i and m <= j) and ( m = i or m =j) Possible: when “m” is smaller than i and j Current program assign smallest value to “m” Question: .
