Design and Analysis of

Algorithm

Tanveer Ahmed Siddiqui

Department of Computer Science

COMSATS University, Islamabad
 Recap and Today
Covered
Algorithm Design and Analysis Process
Understand the problem

Decide on : algorithm
design techniques etc.

Design an algorithm

Prove correctness

Analyze efficiency etc

Code the algorithm

Department of Computer Science
 Today
Covered
After completing this lecture, you will be
able to know
 Proving the Correctness of Algorithms
 Preconditions and Postconditions
 Loop Invariants
 Induction – Math Review
 Using Induction to Prove Algorithms

Department of Computer Science

 Correctness of an
algorithm

Prove the
correctness of
the algorithm

Department of Computer Science

Algorithm design techniques/strategies
 We have discussed the following
designing techniques for developing an
algorithm.
 Using these techniques one can design
an algorithm either Iterative or Recursive.

Department of Computer Science

 What are key parts of an algorithm ?

 Let us quickly revisit the key parts of an

algorithm.
 An algorithm is described by:
 Input data
 Output data
 Preconditions
 Postconditions

Department of Computer Science

 Pre conditions and Post conditions

 PRE-CONDITIONS
 The predicate describing the initial state is
called the pre-condition of the algorithm.
 It indicates what must be true before the
algorithm start.
 Precondition: a predicate I on the input data
 POST-CONDITIONS
 The predicate describing the final state is
called the post-condition of the algorithm.
 It indicates what will be true when the
algorithm finishes its work.
 Post condition: a predicate O on the output
data
Department of Computer Science
 Pre conditions and Post conditions

 Example: Binary Search

 Input data: A:array of integer; x:integer;
 Output data: found: Boolean;
 Precondition: A is sorted in ascending
order
 Postcondition: found is true if x is in A,
and found is false.

Department of Computer Science

 Example 1
 Algorithm to compute square root of
nonnegative integers
 What needs to be true so that Algorithm
successfully carry out its work?
 Since negative numbers don't have a square root,
we need to ensure that the argument, x, is not
negative.
 This requirement is expressed in the pre condition
 Pre-condition: x ≥ 0.
 The post condition is simply a statement
expressing what work has been accomplished by
the function.
 Post-condition: The square root of x has been
written to the standard output.

Department of Computer Science

 Example 2
 Algorithm to compute a product of two
nonnegative integers
 Pre-condition: The input variables m and n are
nonnegative integers.
 Post-condition: The output variable p equals m ·
n.
 Algorithm to find the quotient and remainder
of the division of one positive integer by
another
 Pre-condition: The input variables a and b are
positive integers.
 Post-condition: The output variable q and r are
positive integers such that a = b · q + r and 0 ≤r <
b.
Department of Computer Science
 Pre and Post conditions of a sorting algorithm

 What are the pre-condition and post

condition of a sorting Algorithm
 Pre-condition: The input variable A[1],
A[2], . . . A[n] is a one-dimensional array of real
numbers.
 Post-condition: The input variable B[1],
B[2], . . . B[n] is a one-dimensional array of real
numbers with same elements as A[1], A[2], . . .
A[n] but with the property that B[i] ≤B[j]
whenever i ≤ j.

Department of Computer Science

 Correctness of algorithm
 Once an algorithm has been designed
and specified, we have to prove its
correctness.
 What does correctness of an algorithm
means?
 for any correct input data:
 it stops and

 it produces correct output.

Department of Computer Science

 Correctness of algorithm
 How to ensure correctness of an
algorithm?
 To verify if an algorithms really solves
the problem for which it is designed, we
can use one of the following strategies:
 Experimental analysis (testing).
 Program testing should be limited to a few data
sets only.
 Formal analysis (proving).

Department of Computer Science

 Correctness of algorithm

 Proving that an algorithm is totally correct:

1. Proving that the list of actions applied to the precondition
imply the post condition, i.e. proving I O
2. Proving that it will terminate, i.e., show that loop bounds
cannot increase infinitely.

INDEED this point is reached, AND this is the desired output

Any legal Algorithm Output

input

Department of Computer Science

 UP-SHOT: Correctness of algorithm
 Once an algorithm has been designed
and specified, we have to prove its
correctness.
 What does correctness of an algorithm
means?
 for any correct input data:
 it stops and

 it produces correct output.

 Correct input data: satisfies

precondition
 Correct output data:
Department of Computer Science
 Exchange
Problem
 Problem: Exchange the values of two variables
say x and y
Proof: the list of
actions applied to the
input (which satisfies
the precondition) imply
the output satisfies the
postcondition
 Can you prove its correctness? 1. Precondition: x = a

 Precondition: and y = b
 x = a and y = b 2. temp := x => temp
 Postcondition:
=a
3. x : = y => x = b
 x = b and y = a
4. y := temp => y = a
5. x = b and y = a is
Department of Computer Science
the Postcondition
 Proving correctness

 Proving that the list of actions applied to

the input (which satisfies the
precondition) imply that the output
satisfies the postcondition.
 This is easy to prove for simple sequential
algorithms.
 How we prove the correctness of a
repetitive algorithm?
 We use techniques based on loop invariants
and induction

Department of Computer Science

 Loop invariants and induction

 Induction can be used for proving the

correctness of repetitive algorithms:
 Iterative Algorithms:
 Loop invariants
 Induction hypothesis = loop invariant = relationships
between the variables during loop execution
 Recursive Algorithms
 Direct induction
 induction hypothesis = assumption that each
recursive call itself is correct (often a case for
applying strong induction)

Department of Computer Science

UP-SHOT: correctness of the algorithm

Correctness of
Algorithm

Iterative Algorithm Recursive Algorithm

Loop Invariant Mathematical

Induction

Department of Computer Science

 Loop
Invariant

Department of Computer Science

 Thinking Time
 Consider the following algorithm.
 Identify property of the loop that is
necessarily true immediately before and
immediately after each iteration of the
loop.
 To identify property of the loop that does
not change, let's make trace table

Department of Computer Science

 Trace Table for Multiplication Algorithm
Iteration # Action an in
0 Initial a0 = 0 i0 = 0
Result of Step a1 = a0+ y
1 3(a) a1 = 0+ 5 = 5
Result of Step i1 = i0 +1
3(b) i1 = 0+1 =1
From trace table we can a1 = 5* 1 = y* i1
observed that Result of Step a2 = a1+ y
following property 3(a) a2 = 5+ 5 = 10
2
does not change: Result of Step i2 = i1 +1
3(b) i2 = 1 +1 =2
P(n): an = in . y, n≥ 0 a2 = 5* 2 = y* i2
Where an and in denotes Result of Step a3 = a2+ y
the values of answer 3 3(a) a3 = 10+ 5 = 15
and I at the end of n Result of Step i3 = i2 +1
iterations. 3(b) i3 = 2 +1 =3
a3 = 5* 3 = y* i3
Result of Step a4 = a3+ y
3(a) a4 = 15+ 5 = 20
4 Result of Step i4 = i3 +1 =1
3(b) i4 = 3 +1 =4
a4 = 5* 3 = y* i4
Department of Computer Science
Result answer = 20
 Loop invariants
 Property of loop that does not change is
called Loop Invariant.
 A loop invariant is a condition/predicate
[among program variables] that is
necessarily true immediately before and
immediately after each iteration of a loop.
 Note that this says nothing about its truth
or falsity part way through an iteration.

Department of Computer Science

 Loop invariants
 A loop invariant is some predicate (condition)
that holds for every iteration of the loop.
 Example, let’s look at a simple for loop that looks
like this:

 In this example it is true (for every iteration) that:

i + j == 9.
 A weaker invariant that is also true is that:

i >= 0 && i <= 10.

 One may get confused between the loop invariant, and the loop
conditional ( the condition which controls termination of the loop ).

Department of Computer Science

 Loop invariants
 A loop invariant is a predicate that must
be true.
 before the loop starts
 during each iteration of the loop
 after the loop terminates

Department of Computer Science

 How to define loop invariants

 Good practice define Loop invariant:

 Write carefully the pre-conditions and post-conditions
of the loop.
 Write statement that captures the purpose of the
loop
 Try to find relationship among the variables that
hold true
 just before a loop begins executing.
 after each iteration of the loop.
 after the loop terminates.
 Call this relationship P(n) where n denote the
number of iteration of a loop.

Department of Computer Science

 Example 1:
Trace Table for Multiplication Algorithm
Iteration # Action an in
0 Initial a0 = 0 i0 = 0
Result of Step a1 = a0+ y
1 3(a) a1 = 0+ 5 = 5
Result of Step i1 = i0 +1
3(b) i1 = 0+1 =1
From trace table we can a1 = 5* 1 = y* i1
observed that Result of Step a2 = a1+ y
following property 3(a) a2 = 5+ 5 = 10
2
does not change: Result of Step i2 = i1 +1
3(b) i2 = 1 +1 =2
P(n): an = in . y, n≥ 0 a2 = 5* 2 = y* i2
Where an and in denotes Result of Step a3 = a2+ y
the values of answer 3 3(a) a3 = 10+ 5 = 15
and I at the end of n Result of Step i3 = i2 +1
iterations. 3(b) i3 = 2 +1 =3
a3 = 5* 3 = y* i3
Result of Step a4 = a3+ y
3(a) a4 = 15+ 5 = 20
4 Result of Step i4 = i3 +1 =1
3(b) i4 = 3 +1 =4
a4 = 5* 3 = y* i4
Department of Computer Science
Result answer = 20
 Example 2:

 Find maximum element max in the array.

 Loop invariant: max is always maximum

among the first i elements of array A.

Department of Computer Science 28

 Example 3: Bubble
Sort

Department of Computer Science 29

 Example 3: Bubble
Sort

a: 19 5 12 7 a: 5 12 7 19
0 1 2 3 0 1 2 3

a: 5 19 12 7 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 19 7 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 7 19 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 7 19 a: 5 7 12 19
Department of Computer Science 0 1 30 2 3
0 1 2 3
 Example 3: Bubble
Sort

Department of Computer Science 31

 Example 3: Bubble
Sort
 Pre- Condition: The input variable A[1], A[2], . . .
A[n] is a one-dimensional array of real
numbers.
 Post- Condition: The input variable B[1], B[2], . .
. B[n] is a one-dimensional array of real
numbers with same elements as A[1],
A[2], . . . A[n] but with the property that B[i]
≤B[j] whenever i ≤ j.
 Loop Invariant: Let P(n) = The algorithm sorts every list
of size n ≥ 1

Department of Computer Science

 Brute Force: Selection
Example 4: Selection Sort
Sort

| 89 45 68 90 29 34 17
17 | 45 68 90 29 34 89
17 29 | 68 90 45 34 89
17 29 34 45 | 90 68 89
17 29 34 45 68 | 90 89
17 29 34 45 68 89 | 90
In selection sort algorithm we find the minimum element
from the unsorted part and put it at the beginning.

Department of Computer Science 33

 Brute Force: Selection
Example 4: Selection Sort
Sort

| 89 45 68 90 29 34 17
17 | 45 68 90 29 34 89

In the above pseudo code there 17 29 | 68 90 45 34 89

are two loop invariant condition: 17 29 34 45 | 90 68 89
1.In the outer loop, array is sorted
for first i elements. 17 29 34 45 68 | 90 89
2.In the inner loop, min is always 17 29 34 45 68 89 | 90
the minimum value in A[i … j].
Loop Invariant: Before the start of each loop, A[min] is less than or
equal toweA[i..j-1].
Note that use the notation i..j to denote the set {x | i ≤ x ≤ j} = {i,i+1,...,j-1,j}.
We use the notation a[i..j] to indicate the subsequence of the array a starting from a[i] and
continuing up to and including a[j].
Department of Computer Science 34
 Brute Force: Selection
Example 4: Selection Sort
Sort

| 89 45 68 90 29 34 17
17 | 45 68 90 29 34 89

In the above pseudo code there 17 29 | 68 90 45 34 89

are two loop invariant condition: 17 29 34 45 | 90 68 89
1.In the outer loop, array is sorted
for first i elements. 17 29 34 45 68 | 90 89
2.In the inner loop, min is always 17 29 34 45 68 89 | 90
the minimum value in A[i to j].

Loop Invariant: Before the start of each loop, A[min] is less

than or equal to A[i..j-1].

Department of Computer Science 35

 Example 5: Insertion Sort:

89 | 45 68 90 29 34 17

45 89 | 68 90 29 34 17

45 68 89 | 90 29 34 17

45 68 89 90 | 29 34 17

29 45 68 89 90 | 34 17

29 34 45 68 89 90 | 17

17 29 34 45 68 89 90

Department of Computer Science

 Example 5: Insertion Sort:

89 | 45 68 90 29 34 17

45 89 | 68 90 29 34 17

45 68 89 | 90 29 34 17

45 68 89 90 | 29 34 17

29 45 68 89 90 | 34 17

29 34 45 68 89 90 | 17

17 29 34 45 68 89 90
 Invariant: at the start of each for loop, A[1…j-1] consists of
elements originally in A[1…j-1] but in sorted order
Department of Computer Science
 Example 6: Quick Sort:

 Invariant:
1) All entries in A[p . . i] are ≤ pivot.
2) All entries in A[i + 1 . . j − 1] are > pivot.
3) A[r] = pivot.

Department of Computer Science

 Example 7: Decimal to Binary

 Invariant:
 If m is the integer represented by array b[1..k],
then n=t*2k+m

Department of Computer Science

 Loop invariants and induction

 Proving loop invariants is a form of

mathematical induction:
 showing that the invariant holds before the
first iteration corresponds to the base case,
and
 showing that the invariant holds from iteration
to iteration corresponds to the inductive step.

Department of Computer Science

 How to prove this property?

 We must show the following 3 things

about a loop invariant:
1. Initialization:
 In this step we must show that invariant is
true prior to the first iteration of the loop.
2. Maintenance:
 In this step we must show that if the invariant
is true for ith iteration, it is true for(i+1)th
iteration i.e., next iteration.
3. Termination: When the loop terminates,
the invariant is true on the entire input.

Department of Computer Science

 Examples
Proving
Correctnes
s of
Algorithm

Department of Computer Science

Induction Examples (4/4)Example 1: Multiplication
3.3 Mathematical Induct

 Prove that following algorithm works correctly

Department of Computer Science

 Induction Examples (4/4)Example 1: Multiplication
3.3 Mathematical Induct

 PROOF (by PMI): Let P(n): an = in . y, n≥ 0

 Initialization(Basis Step): The value n =0
means zero iteration; it corresponds to the
situation before the loop is entered.
 When n = 0,
 a0 = 0 (By Statement i)
 and i0 = 0. (By Statement ii)
 Therefore,
 a0 = i0 .y = 0. y =0
 so, P(0) is true

Department of Computer Science

Induction Examples (4/4)Example 1: Multiplication
3.3 Mathematical Induct

 Maintenance(Induction Step): Assume P(k)

is true; that is after k iterations
ak = ik .y
Then,
ak+1 = ak + y (by line 3(a))
and ik+1 = ik + 1 (by line 3(b))
Thus:
ak+1 = ik .y + y (by inductive hypothesis)

= (ik +1) y
= (ik+1).y
So, P(K+1) is true
Department of Computer Science
Induction Examples (4/4)Example 1: Multiplication
3.3 Mathematical Induct

 Termination: When i ≥ x, loop will

terminate

Department of Computer Science

Induction Examples (4/4)Example 2: Factorial
3.3 Mathematical Induct

 Prove that following algorithm works correctly

 Loop Invariant: Let P(n): fact(n) = n!, n≥ 0

Department of Computer Science

Induction Example
Examples 2: Factorial
(4/4) of positive integer
3.3 Mathematical Induct

 PROOF (by PMI): Let P(n): fact(n) = n!, n≥ 0

 Initialization(Basis Step): The value n =0 means
zero iteration; it corresponds to the situation before
the loop is entered.
 When n = 0 , fact(0) = 1=1! (by line 1)
 so, P(0) is true
 Maintenance(Induction Step): Assume P(k) is true;
that is after k iterations
fact(k) = k!
Then fact(k+1) = fact(k).(k+1) (by line 3(b))
Thus:
fact(k+1) = k! .(k+1) (by inductive hypothesis)
= (k+1)!
So, P(K+1) is true
Department of Computer Science
Induction Examples (4/4)Example 1: Multiplication
3.3 Mathematical Induct

 Termination: When i > n, loop will

terminate

Department of Computer Science

 Example 3

 Consider the following algorithm?

 What does this algorithm compute?

 What is its Pre-condition and Post- condition?
 Sate its Loop Invariant, I(n).
 Establish the correctness of given algorithm using loop invariant
define in part (c). You must clearly show all these steps:
initialization, maintenance and termination.

Department of Computer Science

 Example 3

 Consider the following algorithm?

 What does this algorithm compute?

 Answer: This algorithm computes the sum of first n
positive even numbers, i.e. 2+4+6-------+ 2n

Department of Computer Science

 Example 3

 Consider the following algorithm?

 What is its Pre-condition and Post- condition?

 Answer:
 Pre-Condition: n is a nonnegative integer, i = 0, and answer = 0.
 Post-Condition: answer = Sum of the first n positive even integer i.e.
2+4+6-------+ 2n
Department of Computer Science
 Example 3

 Consider the following algorithm?

 Sate its Loop Invariant, I(n).

 Answer: Let S denote the value of sum after n
n
th
iteration, then loop
invariant I(n) for given algorithm can be defined as:
 I(n) : Sn = n(n+1)

Department of Computer Science

 Example 3

1. Initialization:
 In this step we must show that invariant is
true prior to the first iteration of the loop.

Department of Computer Science

 Example 3
1. Maintenance:
 In this step we must show that if the invariant
is true for ith iteration, it is true for(i+1)th
iteration i.e., next iteration.

Department of Computer Science

 Example 3

1. Termination: when the loop terminates,

the invariant is true on the entire input.

Department of Computer Science

 Example 4

Algorithm
Proof: the list of actions
Sum_of_N_numbers applied to the
precondition imply the
Input: a, an array of N postcondition
numbers BUT: we cannot enumerate
Output: s, the sum of the N all the actions in case of
numbers in a a repetitive algorithm !
How to prove
s:=0; repetitive
k:=0; algorithms?
While (k<N) do We use techniques based
k:=k+1; on loop invariants and
s:=s+a[k]; induction
end Iterative algorithms: use
Loop invariants
Recursive algorithms: use
Department of Computer Science induction using as
 Example 4
Loop invariant = induction
Algorithm hypothesis: At step k, S holds the
Sum_of_N_numbers
sum of the first k numbers
Input: a, an array of N 1. Initialization: The
numbers
hypothesis is true at
Output: s, the sum of
the N numbers in a the beginning of the
loop:
s:=0; Before the first iteration:
k:=0;
While (k<N) do s=0, k=0.
k:=k+1; The first 0 numbers have
s:=s+a[k]; sum zero (there are no
end
numbers)
=> hypothesis true before
entering the loop
Department of Computer Science
 Example 4

 Induction hypothesis: S= sum of the first

k numbers
2. Maintenance: If hypothesis is true before
step k, then it will be true before step
k+1 (immediately after step k is finished)
We assume that it is true at beginning of step k:
“S is the sum of the first k numbers”
We have to prove that after executing step k, at
the beginning of step k+1: “S is the sum of
the first k+1 numbers”
We calculate the value of S at the end of this step
k:=k+1, s:=s+a[k+1] => s is the sum of the first
k+1 numbers
Department of Computer Science
 Example 4

 Induction hypothesis: S= sum of the first k

numbers
3. Termination: When the loop terminates,
the hypothesis implies the correctness of
the algorithm
The loop terminates when k=n
 s= sum of first k=n numbers
 post condition of algorithm

DONE

Department of Computer Science

 Example 5

What does it mean for b[0….x] to hold a binary

representation of the number n

Department of Computer Science

 Example 5

Department of Computer Science

 Example 5
Algorithm Decimal_to_Binary
Input: n, a positive
integer Loop invariant: If m is the
Output: b, an array of integer represented by array
bits, the bin repr. of b[1..k], then n=t*2k+m
n,starting with the least
significant bits
t:=n; 1. The hypothesis is
k:=0;
while (t>0) do
true at the
k:=k+1; beginning of the
b[k]:=t mod 2; loop:
t:=t div 2;
end k=0, t=n, m=0(array is
empty)
n=n*2^0+0

Department of Computer Science

 Example 5

 Induction hypothesis: If m is the integer

represented by array b[1..k], then
n=t*2^k+m
2. If hypothesis is true for step k, then it will
be true for step k+1
At the start of step k: assume that n=t*2^k+m,
calculate the values at the end of this step
If t=even then: t mod 2==0, m unchanged,
t=t / 2, k=k+1=> (t / 2) * 2 ^ (k+1) + m =
t*2^k+m=n
If t=odd then: t mod 2 ==1, b[k+1] is set to 1,
m=m+2^k , t=(t-1)/2, k=k+1 =>
(t-1)/2*2^(k+1)+m+2^k=t*2^k+m=n
Department of Computer Science
 Example 5

 Induction hypothesis: If m is the integer

represented by array b[1..k], then
n=t*2^k+m
3. When the loop terminates, the
hypothesis implies the correctness of the
algorithm
The loop terminates when t=0 =>
n=0*2^k+m=m
n==m, proved

Department of Computer Science

 Example 6: Insertion Sort algorithm

 Invariant: at the start for

for j=2
j=2 to
to length(A)
length(A)
do key=A[j]
of each for loop, A[1… do key=A[j]
i=j-1
i=j-1
j-1] consists of while
while i>0
i>0 and
and A[i]>key
A[i]>key
elements originally in do
do A[i+1]=A[i]
A[i+1]=A[i]
A[1…j-1] but in sorted i--
i--
A[i+1]:=key
A[i+1]:=key
order

Department of Computer Science

 Example 6: Insertion Sort algorithm

 Invariant: at the start for

for j=2
j=2 to
to length(A)
length(A)
do key=A[j]
of each for loop, A[1… do key=A[j]
i=j-1
i=j-1
j-1] consists of while
while i>0
i>0 and
and A[i]>key
A[i]>key
elements originally in do
do A[i+1]=A[i]
A[i+1]=A[i]
A[1…j-1] but in sorted i--
i--
A[i+1]:=key
A[i+1]:=key
order
 Initialization: j = 2, the invariant trivially holds
because A[1] is a sorted array 

Department of Computer Science

 Example 6: Insertion Sort algorithm

 Invariant: at the start for

for j=2
j=2 to
to length(A)
length(A)
do key=A[j]
of each for loop, A[1… do key=A[j]
i=j-1
i=j-1
j-1] consists of while
while i>0
i>0 and
and A[i]>key
A[i]>key
elements originally in do
do A[i+1]=A[i]
A[i+1]=A[i]
A[1…j-1] but in sorted i--
i--
A[i+1]:=key
A[i+1]:=key
order

 Maintenance: the inner while loop moves

elements A[j-1], A[j-2], …, A[j-k] one position right
without changing their order. Then the former A[j]
element is inserted into k-th position so that A[k-1]
 A[k]  A[k+1].
A[1…j-1] sorted + A[j] A[1…j] sorted
Department of Computer Science
 Example 6: Insertion Sort algorithm

 Invariant: at the start for

for j=2
j=2 to
to length(A)
length(A)
do key=A[j]
of each for loop, A[1… do key=A[j]
i=j-1
i=j-1
j-1] consists of while
while i>0
i>0 and
and A[i]>key
A[i]>key
elements originally in do
do A[i+1]=A[i]
A[i+1]=A[i]
A[1…j-1] but in sorted i--
i--
A[i+1]:=key
A[i+1]:=key
order

 Termination: the loop terminates, when j=n+1.

Then the invariant states: “A[1…n] consists of
elements originally in A[1…n] but in sorted order”


Department of Computer Science

 Example 7: Bubble
Sort
 Establish the correctness of following
algorithm

Department of Computer Science 70

 Example 7: Bubble
Sort

a: 19 5 12 7 a: 5 12 7 19
0 1 2 3 0 1 2 3

a: 5 19 12 7 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 19 7 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 7 19 a: 5 7 12 19
0 1 2 3 0 1 2 3

a: 5 12 7 19 a: 5 7 12 19
Department of Computer Science 0 1 71 2 3
0 1 2 3
 Example 7: Bubble
Sort

Department of Computer Science 72

 Example 7: Bubble
Sort
 Pre- Condition: The input variable A[1], A[2], . . .
A[n] is a one-dimensional array of real
numbers.
 Post- Condition: The input variable B[1], B[2], . .
. B[n] is a one-dimensional array of real
numbers with same elements as A[1],
A[2], . . . A[n] but with the property that B[i]
≤B[j] whenever i ≤ j.
 Loop Invariant: Let P(n) = The algorithm sorts every list
of size n ≥ 1

Department of Computer Science

 Correctness
Induction Examples (4/4) of Bubble Sort :Proof
3.3 Mathematical Induct

Proof
Basis step: When n =1, the list contains just one element and
hence is clearly sorted, So P(1) is true
Induction Step: Assume P(k) is true; that is, the algorithm sorts
correctly every list of k ( ≥ 1)
To show that P(k+1) is true, consider a list X = [x1, x2 x3, x4…. xk,
xk+1]
Since k+1 ≥ 2 , the for loop in line 1 is entered. When i =0, j
runs from 1 through n-2. Statements in line are executed: the
consecutive elements xj and xj+1 are compared and swapped if
out of order. The inner for loop places the largest of the
elements x1, x2 x3, x4…. xk, xk+1 in position k+1. This leaves a sub
list of k elements, [x1, x2 x3, x4…. xk]. By the inductive hypothesis,
the algorithm correctly sort it. It follows that the algorithm
correctly sorts the
Department of Computer entire list X; that is, P(k+1) is true. Thus, by
Science
 Conclusion

Department of Computer Science

 Conclusion
 Correct input data: satisfies pre-condition
 Correct output data: satisfies post-condition
 Two main conditions for correctness:
 The algorithm is complete/correct: the post-
condition is respected on all possible inputs
satisfying the pre-condition
 Precondition: a predicate I on the input data
 Postcondition: a predicate O on the output data
 Correctness: proving I O
 The algorithm terminates
 For all possible input, the algorithm exits

Department of Computer Science

 Loop Invariant
 Let n denote the number of iteration of a loop.
 Let P(n) be a predicate.
 A relationship among the variables hold true before the
loop is executed and after each iteration of the loop, no
matter how large n is. As the algorithm execution
progresses, the values of the variables in the loop may
vary, but the relationship remains unaffected. Such a
predicate is a loop invariant.
 A loop invariant is a statement about program variable
that is:
 true just before a loop begins executing.
 Also true after each iteration of the loop.
Department of Computer Science
 Correctness of Algorithm
 Induction can be used for proving the
correctness of repetitive algorithms:
 Iterative algorithms:
 Loop invariants

 Induction hypothesis = loop invariant =

relationships between the variables

during loop execution
 Recursive algorithms
 Direct induction

 Hypothesis = a recursive call itself ;

often a case for applying strong

induction

Department of Computer Science

 Loop Invariant and Mathematical Induction
 The method of loop invariants is used to
prove correctness of a loop with respect to
certain pre and post-conditions.
 We can use Mathematical Induction to
prove that an invariant has the desired
behavior.
 The Basis Step proves that invariant is true
before the condition that controls looping is
tested for the first time.
 The Inductive Steps assumes that the invariant
is true and then proves that if the condition that
controls looping is true (so that the loop body is
executed again), the invariant is true after the
loop body executes.

Department of Computer Science

 Conclusion

Department of Computer Science

 Loop Invariant and Mathematical Induction

 Reasoning
Since a loop iterates of Proofof
a finite number
times, the form of mathematical
induction used here proves that a finite
sequence of statement is true, rather
than an infinite sequence of
statements.
 Whether the sequence of statements is
finite or infinite, the steps needed for
the proof by the mathematical
induction are the same.

Department of Computer Science

 Conclusion

Department of Computer Science

 Additional
Slides
For self study
Department of Computer Science
 Additional Slides: Study your self

Review of
Mathemati
cal
Induction

Department of Computer Science

 Introduction to Mathematical Induction?
 Induction is a very important tool in computer
science for several reasons, one of which is the
fact that a characteristic of most programs is
repetition of a sequence of statements.
 To illustrate how induction works, imagine that
you are climbing an infinitely high ladder.
 How do you know whether you will be able to
reach an arbitrarily high rung?

Department of Computer Science

 Introduction to Mathematical Induction?
 Suppose you make the following two assertions about your
climbing abilities:
 I can definitely reach the first rung.
 Once I get to any rung, I can always climb to the next
one up.
 If both statements are true, then by statement 1 you can
get to the first one, and by statement 2, you can get to the
second. By statement 2 again, you can get to the third,
and fourth, etc. Therefore, you can climb as high as you
wish.

Department of Computer Science

 Introduction to Mathematical Induction?
 Suppose you make the following two
assertions about your climbing abilities:
 I can definitely reach the first rung.
 Once I get to any rung, I can always climb to the next one
up.
 If both statements are true, then by
statement 1 you can get to the first one, and
by statement 2, you can get to the second.
By statement 2 again, you can get to the
third, and fourth, etc. Therefore, you can
climb as high as you wish.
 Notice that both of these assertions are necessary for you to
get anywhere on the ladder. If only statement 1 is true, you
have no guarantee of getting beyond the first rung. If only
statement 2 is true, you may never be able to get started.
Department of Computer Science
 Introduction to Mathematical Induction?
 Assume that the rungs of the ladder are
numbered with the positive integers (1,2,3...).
 Now think of a specific property that a
number might have. Instead of "reaching an
arbitrarily high rung", we can talk about an
arbitrary positive integer having that
property. We will use the shorthand P(n) to
denote the positive integer n having property
P. How can we use the ladder-climbing
technique to prove that P(n) is true for all
positive n? The two assertions we need to
prove are:
 1) P(1) is true
 2)offor
Department anyScience
Computer positive k, if P(k) is true, then P(k+1) is true
 Steps in Proving by Induction

Claim: P(n) is true for all n  Z+, for n  n0

1. Basis
 Show formula is true when n = n0
2. Inductive hypothesis
 Assume formula is true for an arbitrary n = k
where, k  Z+ and k  n0
3. To Prove Claim
 Show that formula is then true for k+1
Note: In fact we have to prove
1) P(n0) and
2) P(k)  P(k+1)

Department of Computer Science

 Mathematical Way of Expressing Induction
 Basis step.
Show that proposition P(1) is true.
 Inductive step.
Show that for every positive integer n, the
implication P(n)  P(n+1) is true.
P(n) for a fixed n is called inductive hypothesis.

 [P(1)   n, (P(n)  P(n+1))]   n, P(n)

Department of Computer Science

 What did we show
 Base case: P(1)
 If P(k) was true, then P(k+1) is true
 i.e., P(k) → P(k+1)

 We know it’s true for P(1)

 Because of P(k) → P(k+1), if it’s true for P(1), then it’s true for
P(2)
 Because of P(k) → P(k+1), if it’s true for P(2), then it’s true for
P(3)
 Because of P(k) → P(k+1), if it’s true for P(3), then it’s true for
P(4)
 Because of P(k) → P(k+1), if it’s true for P(4), then it’s true for
P(5)
 And onwards to infinity

 Thus, it is true for all possible values of n

 In other   n, (P(n)
[P(1) words,  P(n+1))]
we showed   n, P(n)
that:

Department of Computer Science 91

 Summary
 Proof by induction involves three main steps
 Proving the base of induction
 Forming the induction hypothesis
 Proving that the induction hypothesis holds true for all
numbers in the domain.

Department of Computer Science

 Example 1

Use mathematical induction to prove

Sn = 2 + 4 + 6 + 8 + . . . + 2n = n(n + 1)
for every positive integer n.

1. Show that the formula is true when n = 1.

S1 = n(n + 1) = 1(1 + 1) = 2 True

2. Assume the formula is valid for some integer k. Use this

assumption to prove the formula is valid for the next
integer, k + 1 and show that the formula Sk + 1 = (k + 1)(k
+ 2) is true.

Sk = 2 + 4 + 6 + 8 + ...
+ 2k = k(k + 1) Assumption

Example continues
Department of Computer Science 93
 Example 1

Sk + 1 = 2 + 4 + 6 + 8 + ...
+ 2k + [2(k + 1)]
=2+4+6+8+ ...
+ 2k + (2k + 2)

= Sk + (2k + 2) Group terms to form Sk.

= k(k + 1) + (2k + 2) Replace Sk by k(k + 1).

= k2 + k + 2k + 2 Simplify.

= k2 + 3k + 2

= (k + 1)(k + 2)

= (k + 1)((k + 1)+1)
The formula Sn = n(n + 1) is valid for all positive integer
values of n.
Department of Computer Science 94
 Quick survey

 I felt I understood the first example of

induction…
a) Very well
b) With some review, I’ll be good
c) Not really
d) Not at all

Department of Computer Science 95

 Example 2
Use mathematical induction to prove for all positive integers
n, n 2 n(n  1)(2n  1)
i
i 1
2 2 2 2 2
1  2  3  4    n 
6
.

(  1)(2(1)  1) 1(2)(2  1) 6
11
S1    1 True
6 6 6
k (k  1)(2k  1)
S k 12  22  32  42    k 2  Assumptio
6 n
S k 1 12  22  32  42    k 2  (k  1)2
S k  (k  1) 2
S k  k 2  2k  1 Group terms to
form Sk.
k (k  1)(2k  1) Replace Sk by k(k
  k 2  2k  1
6 + 1).
Department of Computer Science
Example continues.
96
 Example 2

3 2 2
 2k  3k  k  6k  12k  6 Simplify.
6 6
3 2
 2k  9k  13k  6
6
(k 2  3k  2)(2k  3)

6
(k  1)(k  2)(2k  3)

6
(k  1)[(k  1)  1][2(k  1)  1]

6
The formula S  n(n  1)(2n  1) is valid for all positive
n
6
integer values of n.

Department of Computer Science 97

 Additional Slides: Study your self

Self
reading

Department of Computer Science

 Correctness of algorithm
 What does correctness of an algorithm
means?
 for any correct input data:
 it stops and

 it produces correct output.

Department of Computer Science

 How to ensure correctness of program/algorithm
 In general, one cannot demonstrate the
correctness of the program by simply
taking each of the possible input data,
feeding it to the program, and showing that
the result is correct.
 This situation is akin to a foolish boy sent to the
market to buy a match box and asked to check
the box for any moisture before buying it. The
boy went on lighting one match-stick after
another, till all were burnt. When asked why he
did so, he replied “But then how can I be sure if
the other matches will light?”
 Unfortunately, the computer programmer,
areof Computer
Department in the same situation.
Science
 Correctness of algorithm
 How to ensure correctness of an
algorithm?
 How can they be sure that it will not fail
on a particular data input?
 To verify if an algorithms really solves
the problem for which it is designed we
can use one of the following strategies:
 Experimental analysis (testing).
 Program testing should be limited to a few data
sets only.
 Formal analysis (proving).

Department of Computer Science

 How to ensure correctness of program/algorithm
 To test a program:
 Testing a program consists of two parts
 Debugging( you are familiar with this concept in
programming courses such as Introduction to
programming, OOP, data structure)
 Profiling.
 It is important to be familiar with the
debugging of a program, through what we
refer to here is a more systematic approach
to debugging.
 An interesting observation about debugging,
made by E.W. Dijkstra, a pioneer computer
scientist from Netherlands, is worth quoting
here: “debugging can only point to the presence of
errors and never their absence.”
Department of Computer Science
 Correctness of algorithm
 To validate an algorithm:
 This means that a algorithm/program satisfies its
precise specifications.
 This involves proving the correctness of an
algorithm.
 Taking the story of the foolish boy a little
further, he could have argued that if the
box had absorbed moisture, then there was
a good probability that all the match-sticks
would be equally moist.
 So if he had tasted any one of them, it
should tell him about the whole box.
 Thus he could have used limited testing plus
proof
Department instead
of Computer Science of exhaustive testing.
 Correctness of algorithm
 In this course, we shall discuss the basics of
such proofs for program/algorithm.
 In fact, we shall go a little beyond that – we
shall talk about a method of developing
programs/algorithms where the proof, that
whatever is done till now is correct, will be
developed along with the program/algorithm.
 Experience has shown that this method of
program/algorithm development is the most
promising one.
 Note: Once an algorithm is shown to be
correct, only then should the program coding
begin.
Department of Computer Science
 Correctness of algorithm
 The program also has to be verified by
profiling.
 Profiling is a process of executing a correctly
working program with the appropriate data
sets, and measuring the time and memory
space it takes to execute various parts of the
program.
 These results are useful in improving the
program or even the algorithm.

Department of Computer Science

 Significance and importance of algorithm
correctness
 Why there is so much concern about
program correctness?
 Software errors are costly
 There are many application where an
erroneous program/algorithm can lead to loss
of money( Fig 1)

 of Computer Science
Department
Source : Times of india, July 2001
 Significance and importance of algorithm
correctness
 There are many situations where safety
to human life is involved, like in medical
applications, or industrial safety systems,
atomic power plants, manned space
flights, and so on.
 In these applications, program/algorithm
correctness has to be guaranteed.
 Imagine what will happen if the computer
inside Ghouri missile has an unreliable
program due to which the missile goes hay
wire – it may turn around and strike its own
city rather than the enemy site!

Department of Computer Science

 Correctness of algorithm
 How to ensure correctness of an
algorithm?

Correctness of
Algorithm

Iterative Algorithm Recursive Algorithm

Loop Invariant Mathematical

Induction
Department of Computer Science
Basic steps in algorithms correctness verification
 The main steps in the formal analysis of
the correctness of an algorithm are:
 Identification of the properties of input
data(I) (the so-called problem's pre-
conditions).
 Identification of the properties which must
be satisfied by the output data(O) (the so-
called problem's post-conditions).
 Proving that starting from the
preconditions and executing the actions
specified in the algorithms one obtains the
post-conditions. i.e. proving I O

Department of Computer Science

 Pre- condition
and
Post-
condition

Department of Computer Science

 Predicate
 A predicate is a sentence that contains a
finite number of variables.
 The domain of a predicate variable is the
set of all values that may be substituted in
place of the variable.
 Example: Consider the sentence
 “Aslam is a student at COMSATS ISLAMABAD.”
 Let P:“is a student at the COMSATS
ISLAMABAD”
 Let Q: “is a student at.”
 Then both P and Q are predicate symbols.

Department of Computer Science

 Predicate
 The sentences “x is a student at the
COMSATS ISLAMABAD” and “x is a
student at y” are symbolized as:
 P(x): x is a student at the COMSATS ISLAMABAD”
 Q(x, y): x is a student at y”
where x and y are predicate variables and take values in
appropriate sets.
 When concrete values are substituted in place
of predicate variables, a statement results.
 When we analyze the correctness of an
algorithm a useful concept is that of state.
 The algorithm's state is the set of the values
corresponding to all variables used in the
algorithm.
Department of Computer Science
 Pre conditions and Post conditions

 PRE-CONDITIONS
 The predicate describing the initial state is
called the pre-condition of the algorithm.
 It indicates what must be true before the
algorithm start.
 Precondition: a predicate I on the input data
 POST-CONDITIONS
 The predicate describing the final state is
called the post-condition of the algorithm.
 It indicates what will be true when the
algorithm finishes its work.
 Post condition: a predicate O on the output
data
Department of Computer Science
 Precondition/Postcondition

 Suppose that you are the head of a

programming team. Your team is writing a
large piece of software, perhaps with
millions of lines of code.
 Certainly nobody can keep all those lines of
code in their head at once.
 So, the large problem is broken into smaller
problems. Those smaller problems might be
broken into still smaller problems, and so
on, until you reach manageable problems.
 Each of the manageable problems can be
solved by a module/function but you won't
be writing all these modules/functions.
Department of Computer Science
 Pre and Post conditions
 The modules/functions are written by members of
your team. As each team member is given a
module/function to write, you will specify the
requirements of the module/function by indicating
what the function must accomplish. But most of
the details about how a module/ function work will
be left up to the individual programmers.
 Consider an algorithm that is designed to produce a
certain final state from a given state. Both the initial
and final states can be expressed as predicates
involving the input and output variables.
 There are many ways to specify the requirements
for a module/function. In this lecture we will use a
pair of statements for each algorithm, called the
algorithm's precondition and post condition.
Department of Computer Science
 Example 1
 Algorithm to compute square root of
nonnegative integers
 What needs to be true so that Algorithm
successfully carry out its work?
 Since negative numbers don't have a square root,
we need to ensure that the argument, x, is not
negative.
 This requirement is expressed in the pre condition
 Pre-condition: x ≥ 0.
 The post condition is simply a statement
expressing what work has been accomplished by
the function.
 Post-condition: The square root of x has been
written to the standard output.

Department of Computer Science

 Example 2
 Algorithm to compute a product of two
nonnegative integers
 Pre-condition: The input variables m and n are
nonnegative integers.
 Post-condition: The output variable p equals m ·
n.
 Algorithm to find the quotient and remainder
of the division of one positive integer by
another
 Pre-condition: The input variables a and b are
positive integers.
 Post-condition: The output variable q and r are
positive integers such that a = b · q + r and 0 ≤r <
b.
Department of Computer Science
 Pre and Post conditions of a sorting algorithm

 What are the pre-condition and post

condition of a sorting Algorithm
 Pre-condition: The input variable A[1],
A[2], . . . A[n] is a one-dimensional array of real
numbers.
 Post-condition: The input variable B[1],
B[2], . . . B[n] is a one-dimensional array of real
numbers with same elements as A[1], A[2], . . .
A[n] but with the property that B[i] ≤B[j]
whenever i ≤ j.

Department of Computer Science

 Correctness of algorithm

 What does correctness of an algorithm

means?
 for any correct input data:
 it stops and

 it produces correct output.


Types
 PartialCorrectness
 Total Correctness

Department of Computer Science

 Partial Correctness

What does correctness of an algorithm


means?
Partial correctness
THEN this is the desired outpu
IF this point is reached,

Any legal Algorithm Output

To prove
input
partial correctness
we associate a number of assertions
(statements about the state of the
execution) with specific checkpoints in
the algorithm.
e.g., A[1], …, A[k] form an increasing
sequence
Department of Computer Science
 Total Correctness

What does correctness of an algorithm

means?
 Total
correctness
INDEED this point is reached,AND this is the desired outpu

Any legal Algorithm Output

input
 Proving that an algorithm is totally correct:
1. Proving that the list of actions applied to the
precondition imply the post condition, i.e.
proving I O
2. Proving that it will terminate, i.e., show that loop
bounds cannot increase infinitely.
Department of Computer Science
  Giving credit where credit is due:
 These slides are from following reference
books

Department of Computer Science

 Learning
Outcomes
After completing this lecture you will be able to understand:
 Assertion and their role
 Assertion at Input and Output of Blocks
 Symbolic Execution
 Proof Rules and their Notation
 How Proof Rules are specified for standard High
Language constructs
 Compound Statement

 Conditional Statement

 Case Statement

 Repetitive statement

 Loop invariant and PMI

 Examples
 How to ensure correct termination of program/algorithm
 Examples
Department of Computer Science
 Checking the correctness of the
algorithm
 Once an algorithm has been specified,
you have to prove its correctness which
is one of the difficult, but essential task
in algorithm development.
 The correctness of algorithm means the
correctness of the logic/steps of the
algorithm.
 Generally, algorithm will have many steps,
branching and loops, which are included in
different modules. One has to verify whether
each and every module is working for every
legitimate input in a finite amount of time.

Department of Computer Science

 Checking the correctness of the
algorithm
 Correctness of algorithm can be
confirmed by the uses of some:
 inference rules: propositional logic and its rules(the
rules of inference ) can be used to verify the
correctness of programs

Department of Computer Science

 Assertion at Input and Output of Blocks
 An assertion is a logical statement or
expression which is true.
 It is normally written as a predicate(a
condition or a relation) on the program
variable.
 Input assertion: should be specify the
constraints that have been put on the input
variable of the programming block.
 Output assertion: should specify the results
that the program block is required to generate,
for any input data satisfying the input data.

Department of Computer Science

 Assertion at Input and Output of Blocks
 Suppose a block of an algorithm S,
calculates the quotient and remainder of
two positive numbers x and y. Then
 The input assertion(aka pre-condition)
may be:
 x≥0,y>0
 Output assertion(aka post-condition) may
be:
 (x = q.y + r) and (r < y)

Department of Computer Science

 Correctness of algorithm
 Now the program/algorithm verification is
formulated as a set of implications,
which are to be shown to be true.
 These implications have the general
form:

 P Q 
 Where the logical connectives denotes
‘implies’

Department of Computer Science

 How to ensure correctness of program/algorithm
 To express the information contained in
fig in a more concise form, we shall
express it in general form as:
 {I} S {O}, where
 I : precondition
 O : post condition
 S : Programming language statement
 Or
 The second way writing can

be taken to mean “implication

via S
Department of Computer Science
 How to ensure correctness of program/algorithm

 The second way writing can be taken to mean “implication via S. This is a program specification with the
following meaning

 For our example :

 {( x ≥ 0 , y > 0)}S{(x = q.y + r) and (r < y)}

If the relation I is true before S is executed,

then O will hold upon the completion of S.
In other words if I holds at the entry point of
S, O hold at the exit point of S.

Department of Computer Science

 Rule of Inference and Program Correctness
 Proof Rule Notation are generally expressed as:
 H1, H2, ………….Hn/ H
 Where H1, H2, and so on are propositions, containing
program specifications and other assertions and so is H.
 The meaning or the interpretation of the rule is:
 If H1, H2,……….are all true then H is also true.
 That is (H1 H2  H3  . . .  Hn)  H is a tautology.

 For example, {P}S{R}, R Q / {P} S{Q}
 Or P S  R, R  Q  P S  Q
 As seen from this example, the second notation is
more flexible

Department of Computer Science 131

 Proof Rule: Axiomatic Semantics
 A popular nomenclature used for expressing the
meaning of an algorithm using proof rules is
Axiomatic Semantics.
 Before we develop proof rules for the various
structure programming constructs, let us take
simple example of division algorithm.

Department of Computer Science 132

 Rule of Inference and Program Correctness
 Several rules of inference are useful in proving
program correctness
 The first of these is called the composition rule,
which in essence states that a program is correct
if each of its subprograms is correct

Department of Computer Science 133

 Axiomatic Semantics
 Several rules of inference are useful in proving
program correctness
 The first of these is called the composition rule,
which in essence states that a program is correct
if each of its subprogram is correct

Department of Computer Science 134

 Top down strategy
 Note that the program specification {P} S {Q} is
partially correct because if P is true, then Q holds,
provided the block S executes and terminates.
 Note that the notion of partial correctness has nothing to do
with whether a program terminates; it focuses only on whether
the program does what it is expected to do if it terminates.
 If we can show in addition that the program S
terminates for all values of the input satisfying the
relation P, then the program is totally correct.
 Our approach follow the steps of top down strategy:
 Start with top level program specification {P}S{Q}, specifying
the pre-condition P and the post-condition Q clearly.
 The process of top down strategy yields blocks Si with program
specifications {Pi}Si{Qi}
 The design of the program goes hand in hand with the proofs
of correctness of these various specification.
Department of Computer Science 135
 Composition
Top Rule
down strategy

 Stated mathematically, the composition

rule is:
p{S1}q
q{S2}r
---------------
 p{S1;S2}r

Department of Computer Science 136

 Composition Rule

 Suppose a program S is split into

subprograms S1 and S2
 the notation S=S1;S2 indicates S is made up of S1
followed by S2
 Suppose S1 and S2 can each be proven
partially correct with respect to assertions p,
q and r - then we have p{S1}q and q{S2}r
 Thus, if p is true and S=S1;S2 executes and
terminates, then r is true

Department of Computer Science 137

 Conditional Statement

 Conditional statements are program

segments of the form: if condition then S
(where S is a block of statements)
 When condition is true, S is executed
 When condition is untrue, S is not executed

Department of Computer Science 138

 Conditional Statement

 To verify the segment is correct with

respect to initial assertion p and final
assertion q:
 show that when p is true and condition is true,
then q is true after S terminates
 show that when p is true and condition is
false, then q is true (that is, S does not
execute)

Department of Computer Science 139

 Rule of Inference for Conditional Statement

(p  B){S}q
(p  B)  q
-------------------------------------
 p{if condition then S}q

Department of Computer Science 140

 Example
 Verify that the following program segment
is correct with respect to initial assertion
p=T and final assertion q = y  x:
if x > y then y := x
 Since p=T, we need only check condition:
 if x > y is true, y := x; thus y  x, so q is true
 if x > y is not true, then y  x, so q is true
 The program is correct with respect to
given p and q

Department of Computer Science 141

 More complex conditional statements

 With a statement of the form:

if condition then S1 else S2
the logic is somewhat more complicated: if
condition is true, S1 executes; if condition is
untrue, S2 executes

Department of Computer Science 142

 Verifying more complex conditional statements

 To verify segment correct with respect to

initial assertion p and final assertion q:
 show that when p is true and condition is true,
q is true after S1 terminates;
 show that when p is true and condition is
false, q is true after S2 terminates

Department of Computer Science 143

Rule of inference for complex conditional statements

(p  B){S1}q
(p  B){S2}q
----------------------------------------------
 p{if condition then S1 else S2}q

Department of Computer Science 144

 Example

is correct with respect to initial

assertion y=3 and final assertion z=6

Department of Computer Science 145

 Example
 Let p and q be the initial and final assertion,
then:
 p : y=3 , and q=6
 Start by assuming p is true: that is, y=3
 The assignment statements preceding the
conditional set x to 2 and z to the sum of x
and y, or 5
 Since y=3 and 3>0, the condition is true, and
the assignment statement sets z to z+1, or 6
 So at the end, z=6 and q is true

Department of Computer Science 146

 Case Statement

 The case statement is essentially a group

of if then else statement, so write its proof
rule yourself.

Department of Computer Science 147

 Loops: while loop

 A loop is a statement of the form:

 while condition S
 where S is executed repeatedly until condition
becomes false

Department of Computer Science 148

 Rule of inference for while Loop

 If P holds, when we first entered the while-loop, it is clear

that P ∧ B will hold if we get to point C.
 Thus, if we want to assure that P remains true when we
return to point A, we want to be sure that {P ∧ B} S {P}
was established for S.
 Then P will hold at point A, for an arbitrary number of
iterations of the loop.
 Also, P ∧ B holds every time at C.
 When the loop terminates,
P ∧ ¬B holds at the point D.
 So, we get our proof rule:

Department of Computer Science 149

 Rule of inference for Loops

(p  condition){S}p
----------------------------------------------
 p{while condition S}(condition  p)

Department of Computer Science 150

 Rule of inference for do while Loop

 DYS

Department of Computer Science 151

 Proving correctness of entire programs

 Split the program into segments: the rule

of composition can be used to build the
correctness proof
 Prove the correctness of each segment:
for example, if there are 4 segments,
prove p{S1}q, q{S2}r, r{S3}s, and s{S4}t
 If all are true, then p{S}t is true
 If all 4 segments terminate, then S
terminates, and correctness is proven

Department of Computer Science 152

 Example

 Prove correctness of following algorithm.

 What we have to prove is

Department of Computer Science 153

 Example

 Prove correctness of following algorithm.

Department of Computer Science 154

 Example

 Prove correctness of following algorithm.

Department of Computer Science 155

 Example

 Then to verify S3, we have to show that

 Here S2 is given by

Department of Computer Science 156

 Example

Department of Computer Science 157