Chapter 4 (Part 3):
Mathematical Reasoning, Induction & Recursion
Recursive Algorithms (4.4)
Program
Correctness (4.5)
by Kenneth H. Rosen, Discrete Mathematics & its Applications, Sixth Edition, Mc Graw-Hill, 2007
Recursive Algorithm (4.4)
Goal: Reduce the solution to a problem with a particular set of input to the solution of the same problem with smaller input values Example: Greater Common Divisor (gcd) gcd(a,b) = gcd(b mod a, a) gcd(4,8) = gcd(8 mod 4, 4) = gcd(0,4) = 4
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Definition 1: An algorithm is called recursive if it solves a problem by reducing it to an instance of the same problem with smaller input.
Example: Give a recursive algorithm for computing an; a 0, n>0 Solution: an+1 = a*an for n>0 a0 = 1
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
A recursive algorithm for computing an
Procedure power(a: nonzero real number, n: nonnegative integer) if n = 0 then power(a, n):= 1 Else power(a,n) := a * power(a, n-1)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Example: Give a recursive algorithm for computing the greatest common divisor of two nonnegative integers a and b (a<b) Solution: gcd(a,b) = gcd(b mod a, a) and the condition gcd(0,b) = b (b>0).
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
A recursive algorithm for computing gcd(a,b)
procedure gcd(a, b: nonnegative integers with a<b) if a = 0 then gcd(a,b) := b else gcd(a,b) := gcd(b mod a, a)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Example: Express the linear search as a recursive procedure: search x in the search sequence aiai+1 aj. A Recursive linear search algorithm
procedure search(i, j, x) if ai = x then location := i else if i = j then location := 0 else search(i + 1, j,x)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Recursion
We
& iteration
need to express the value of a function at a positive integer in terms of the value of the function at smaller integers Compute a recursive procedure for the evaluation of n!
Example:
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
A
recursive procedure for factorials
procedure factorial(n: positive integer if n = 1 then factorial(n) := 1 else factorial(n) := n * factorial(n - 1)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Recursion
However,
10
& iteration (cont.)
instead of reducing the computation to the evaluation of the function at smaller integers, we can start by 1 and explore larger in an iterative way
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
An
11
iterative (vs. recursive) procedure for factorials
procedure iterative factorial(n: positive integer) x := 1 for i := 1 to n x := i * x {x is n!}
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
Recursion
An
12
& iteration (cont.)
other example is the recursive algorithm for Fibonacci numbers
procedure fibonacci(n: nonnegative integer) if n = 0 then fibonacci(0) := 0 else if n = 1 then fibonacci(1) := 1 else fibonacci(n) := fibonacci(n 1) + fibonacci(n 2)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Recursive algorithm (4.4) (cont.)
13
An iterative algorithm for computing Fibonacci numbers
procedure iterative fibonacci(n: nonnegative integer) if n = 0 then y := 0 else begin x := 0 y := 1 for i := 1 to n 1 begin z := x + y x := y y := z end end {y is the nth Fibonacci number}
Program Correctness (4.5)
14
Introduction
Question: How can we be sure that a program always produces the correct answer?
The syntax is correct (all bugs removed!) Testing a program with a randomly selected sample of input data is not sufficient Correctness of a program should be proven! Theoretically, it is never possible to mechanize the proof of correctness of complex programs We will cover some of the concepts and methods that prove that simple programs are corrects
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
15
Program verification
To prove that a program is correct, we need two parts:
1. For every possible input, the correct answer is obtained if the program terminates 2. The program always terminates
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
Program
16
verification (cont.)
Definition 1: 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.
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
17
This definition of partial correctness (has nothing to do whether a program terminates) is due to Tony Hoare Example: Show that the program segment y := 2 z := x + y is correct with respect to the initial assertion p: x =1 and the final assertion q: z =3. Solution: p is true x = 1 y := 2 z := 3 partially correct w.r.t. p and q
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
18
Rules of inference
Goal: Split the program into a series of subprograms and show that each subprogram is correct. This is done through a rule of inference. The program S is split into 2 subprograms S1 and S2 (S = S1; S2)
Assume that we have S1 correct w.r.t. p and q (initial and final assertions) Assume that we have S2 correct w.r.t. q and r (initial and final assertions)
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
19
It follows: if p is true (S1 executed and terminates) then q is true if q is true (S2 executed and terminates) then r is true thus, if p = true and S = S1; S2 is executed and terminates then r = true This rule of inference is known as the composition rule.
It is written as: p {S1}q q {S2}r
p {S1; S2) r
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
20
Conditional Statements
Assume that a program segment has the following form:
1. if condition then S where S is a block of statement
Goal: Verify that this piece of code is correct
Strategy: a) We must show that when p is true and condition is also true, then q is true after S terminates b) We also must show that when p is true and condition is false, then q is true
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
21
We can summarize the conditional statement as: (p condition) {S}q (p condition) q p {if condition then S) q
Example: Verify that the following program segment is correct w.r.t. the initial assertion T and the final assertion yx if x > y then y:= x
Solution: a) If T = true and x>y is true then the final assertion y x is true b) If T = true and x>y is false then x y is true final assertion is true again
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
2. if condition then S1 else S2 if condition is true then S1 executes; otherwise S2 executes This piece of code is correct if: a) If p = true condition = true q = true after S1 terminates b) If p = true condition = false q = true after S2 terminates (p condition) {S1}q (p condition) {S2}q p {if condition then S1 else S2) q
22
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
23
Example: Check that the following program segment if x < 0 then abs := -x else abs := x is correct w.r.t. the initial assertion T and the final assertion abs = |x|.
Solution: a) If T = true and (x<0) = true abs := -x; compatible with definition of abs b) If T = true and (x<0)= false (x 0) = true abs := x; compatible with abs definition.
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
24
Loop invariants
In this case, we prove codes that contain the while loop: while condition S Goal: An assertion that remains true each time S is executed must be chosen: Such an assertion is called a loop invariant. In other words, p is a loop invariant if: (p condition) {S}p is true If p is a loop invariant, then if p is true before the program segment is executed, p and condition are true after termination, if it occurs. We can write the rule of inference as: (p condition) {S}p
p {while condition S} (condition p)
Program Correctness (4.5) (cont.)
25
Example: Determine the loop invariant that verifies that the following program segment terminates with factorial = n! when n 0. i := 1 factorial := 1 While i < n begin i := i + 1 factorial := factorial * i end
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
Solution: Choose p = (factorial = i! (i n)) a) Prove that p is in fact a loop invariant b) If p is true before execution, p and condition are true after termination c) Prove that the while loop terminates
26
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
a) P is a loop invariant:
27
Suppose p is true at the beginning of the execution of the while loop and the while condition holds; factorial = i! i < n
inew = i + 1
factorialnew = factorial * (i + 1) = (i + 1)! = inew!
Since i < n inew = i + 1 n
p true at the end of the execution of the loop p is a loop invariant
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
Program Correctness (4.5) (cont.)
b) Before entering the loop, i = 1 n and factorial :=1 = 1! = i! (i n) (factorial = i!) = true p = true
28
Since p is a loop invariant through the inference rule, if the while loop terminates p = true and i < n false i = n and factorial = i! = n! c) While loop terminates: Because p is a loop invariant, the rule of inference implies that if the while loop terminates, it terminates with p true and with i<n false. In this case, at the end, factorial = i! and i<=n are true, but i<n is false, in other words, i=n and factorial= i!=n!, as desired.
CSE 504 Discrete Structures & Foundations of Computer Science, Chapter 4 (Part 3)
