COL100 �Introduction to Computer Science

Lecture 24 – Correctness and Termination

April, 2024

Semester II

2024-2025

Vireshwar Kumar, Aaditeshwar Seth

CSE@IITD

Agenda

• Need for Correctness and Termination Proofs

​

• Example: GCD

​

• Example: Fibonacci Sequence

​

• Take Home Message

2

Disclaimer: The contents of these slides are taken from various publicly available resources such as books, talks and lectures. They are being used for the purpose of classroom teaching and academic dissemination only. The sources are acknowledged wherever possible.

Algorithm

• A finite specification of the solution to a given problem using the primitives of the computing tool.

​

• It specifies a definite input and output

​

• It is unambiguous

​

• It specifies a solution as a finite process, i.e., the number of steps in the computation is finite

3

Recall Long Multiplication Algorithm

4

Can you prove its correctness?

Correctness Proof

5

Algorithm Validity

• Are all valid mathematical function definitions lead to valid algorithm also?

6

Algorithm Validity

• Are all valid mathematical function definitions lead to valid algorithm also?

​

• Not necessary!

7

Algorithm Validity

• Are all valid mathematical function definitions lead to valid algorithm also?

​

• How about the following definition?

8

Algorithm Validity

• Are all valid mathematical function definitions lead to valid algorithm also?

​

• Why the following definition not a valid algorithm?

9

Algorithm Validity

• Are all valid mathematical function definitions lead to valid algorithm also?

​

• Why the following definition not a valid algorithm? Non-Terminating

10

Another Example

• Not a valid algorithm, since the definition does not tell us how to evaluate the function.

11

Algorithms

• Thus, for all our algorithms, we need to prove

​

• Correctness

​

• Termination

12

Example: GCD

13

Proving Correctness

14

Proving Correctness

15

Proving Correctness

16

Proving Correctness

17

Both the cases are proved.

Hence, the mathematical definition is a correct algorithm

Proving Termination

18

Example: Fibonacci Sequence

19

More Efficient Fibonacci Computation

20

Comparison

21

def fib(n):

global ops

global calls

calls += 1

if n <= 1:

return n

else:

ops += 3

return fib(n - 1) + fib(n - 2)

​

def fiba(n, a, b):

global ops

global calls

calls += 1

if n == 0:

return a

elif n == 1:

return b

else:

ops += 2

return fiba(n - 1, b, a + b)

for n in range(4, 25):

calls = 0

ops = 0

print(fib(n), calls, ops)

​

calls = 0

ops = 0

print(fiba(n, 0, 1), calls, ops)

print()

Comparison

22

def fib_avoid_duplication(n):

global fib_vals

global ops

global calls

calls += 1

if n <= 1:

return n

else:

if (n - 1) not in fib_vals.keys():

fib_vals[n - 1] = fib_avoid_duplication(n - 1)

if (n - 2) not in fib_vals.keys():

fib_vals[n - 2] = fib_avoid_duplication(n - 2)

ops += 3

fib_vals[n] = fib_vals[n - 1] + fib_vals[n - 2]

return fib_vals[n]

for n in range(4, 25):

calls = 0

ops = 0

fib_vals = {}

print(fib_avoid_duplication(n), calls, ops)

print()

Proving Correctness of Efficient Version

23

Proving Correctness of Efficient Version

24

Proof Attempt by Induction

25

Intuitive Understanding

26

Intuitive Understanding

27

Claim

28

Proving the Claim by Induction

29

Take Home Message

• We tried to prove correctness of non-trivial GCD and Fibonacci algorithms.

​

• Our attempts to prove the correctness show that
• Certain obvious and direct approaches may not always work.

​

• An algorithm may have subtle generalizations (or even properties) which may need to be established before we attempt to prove correctness.

​

• Coming up with such generalized claims is crucial to justify the correctness of the algorithm.

30

Take Home Message

• Getting the right generalizations requires hard work and intuition about the algorithm.

​

• In certain cases, designing a new algorithm often requires studying the properties and proving fresh claims based on properties.

​

• The only way to convince ourselves about the correctness of our algorithm is to prove it as we do in mathematics.

​

• The process of coming up with alternative algorithms and proving their correctness requires a degree of creativity.

​

• Herein lies one of the major contributions in the field of computer science.

31