Program Correctness and Recurrence Relations
CSI 2101: Discrete Structures
School of Electrical Engineering and Computer Science, University of Ottawa
March 11, 2022
Copyright By PowCoder代写 加微信 powcoder
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 1 / 10
1 Program Correctness
2 Recurrence Relations
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 2 / 10
Program Verification
A program is said to be correct if it produces the correct output for every possible input.
Definition
A program, or program segment, S is said to be partially correct with respect to the initial assertion p and the final assertion q if whenever p is true for the input values of S and S terminates, then q is true for the output values of S. The notation p{S}q indicates that the program, or program segment, S is partially correct with respect to the initial assertion p and the final assertion q.
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 3 / 10
Rules of Inference
Composite Rule
A useful rule of inference proves that a program is correct by splitting the program into a sequence of subprograms and then showing that each subprogram is correct.
• Suppose a program S is split into subprograms S1 and S2. It is written as S = S1; S2 to indicate that S is made up of S1 followed by S2.
• An example of the composite rule:
p{S1}q (correctness of S1 w.r.t. initial assert. p and final assert. q)
q{S2}r (correctness of S2 w.r.t. initial assert. q and final assert. r) ∴ p{S1; S2}r
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 4 / 10
Conditional Statements
Program segment:
if condition then
Here S is a block of statements.
To verify:
(p ∧ condition){S}q (S is executed if condition is true)
(p ∧ ¬condition) → q (S is not executed if condition is false)
∴ p{if condition then}q
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 5 / 10
Loop Invariants
Program segment
while condition
Here S is repeatedly executed until condition becomes false.
Loop Invariant: An assertion that remains true each time S is executed. If p is a loop invariant, p is true before the program segment is executed,
p and ¬condition are true after termination, if it occurs. (p ∧ condition){S}p
∴ p{while condition S}(¬condition ∧ p)
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 6 / 10
procedure multiply(m,n: integers)
x := x + m
if n < 0 then a := −n else a := n
k := k + 1
if n < 0 then product := −x
else product := x return product
{product equals mn}
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 7 / 10
Applications of Recurrence
A wide range of applications including
• Modeling of genetic statistics/population growth • Solving puzzles/open problems in computations • Dynamic programming/scheduling algorithms
• Financial modeling
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 8 / 10
Solving Recurrence
Recurrence relations are given by equations and their corresponding initial conditions.
The solution to a recurrence relation is a sequence that satusfies the given equation and its initial conditions.
The minimal number of moves requires for the Tower of Hanoi with n disk
is given by
Hn = 2Hn−1 + 1
Initial condition H1 = 1. Solution Hn = 2n − 1
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 9 / 10
Thank You!
Questions and Comments?
Md. Hasan (uOttawa) Discrete Structures 5c MdH W22 March 11, 2022 10 / 10
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com