Transcript 1. Correctness

Correctness of Algorithms
Guilin Wang
The School of Computer Science
3 Nov 2009 (L11)
Sumber dari : www.uow.edu.au/~guilin/teaching/ICS/Lectures/L11ICS-Slides.ppt
Outline

Correctness
-

Introduction
Induction
Assertions
Termination
Nonprocedural Algorithms
- Brief Introduction
(Functional programming & Logic programming)
2
1. Correctness: Introduction
■ Correctness is a very important issue for all algorithm
designers.
■ Unfortunately, most computer programs contain errors,
or bugs.
■ Those bugs could cause programs to fail in certain
circumstances, though they may work well usually.
■ Indeed, programmers spend much efforts for
debugging (finding and correcting bugs in their
programs).
■ So, how can we guarantee that an algorithm or a
program carries out the desired process?
3
1. Correctness: Introduction
Here, we shall discuss the following topics:
■ The meaning of correctness
■ Different types of correctness
■ Methods of increasing our confidence that an
algorithm /program is correct
4
1. Correctness: Introduction
Correctness of an algorithm or program is related
to its purpose (the process to be carried out).
■ A set of beliefs about the purposes of an algorithm is
called the specifications of this algorithm.
■ We say an algorithm is correct w.r.t. its specifications if
it produces the desired results for all input data defined
by the specifications.
■ However, determining whether or not a program is
correct w.r.t. its specification is a non-computable
problem.
5
1. Correctness: Introduction
Several facets of correctness:
■ Partial correctness: When an algorithm
terminates, the results produced is the one
expected.
■ Totally correctness: A partially correct
algorithm, which always terminates.
■ Feasibility: Resource bounds, which may
appear as part of specifications.
6
1. Correctness: Introduction
For producing programs without bugs, or with
fewer bugs (i.e., showing its correctness), we
have two main kinds of methods: Testing and
Proving.
■ Testing: Executing a program on a particular
set of data (called test data).
- Useful and easy to do.
- Not very reliable, as from testing we only know the
effect of a program on the limited test data.
7
1. Correctness: Introduction
■ Proving: Certifying the correctness of a
program on all permissible input data.
- More reliable but usually more difficult.
- The proof for correctness may contain mistakes.
- Experience has shown that even short, informal proofs
can significantly increase our confidence in a program’s
correctness.
- Except crucial applications, producing extremely formal
proof is an expensive (tedious and also challenging)
exercise.
- So, for most applications, we need some balance.
8
1. Correctness: Introduction
■ An informal proof of correctness is just a representation
of well understanding of the program at hand.
- A good practice is to write down useful remarks when
an algorithm is designed. This procedure is also called
documentation or desk-checking.
■ To increase our confidence about the correctness of an
algorithm, we can make such an informal proof more
formal by adding more details.
9
1. Correctness: Induction
Induction is a very useful technique to show the
correctness of an algorithm/program.
■ Inductive Hypothesis: The purpose is to prove that a
statement is true in every case under consideration.
■ Basis: First, we prove that the statement is true for for a
small case.
■ Inductive step: Then, we show that if the statement is
true for a particular case, it is also true for the next
larger case.
■ Conclusion: The statement must be true for every
case.
10
1. Correctness: Induction
Example 1: How to show the following algorithm is partially
correct?
module exponentiate(x)
{Output 2x assuming x is a non-negative integer}
set SUM equal to 1.
repeat x times
set SUM equal to SUM+SUM
{(A) If the nth time this point is reached, SUM will equal 2n}
endrepeat
output SUM
endmodule
11
1. Correctness: Induction
We now use induction to prove the partial
correctness of the above algorithm.
Inductive hypothesis: Once point A is reached for n
times, SUM= 2n.
Basis: When n=1, SUM is set to 1+1, which equal repeat
21.
Inductive step: If the inductive hypothesis is true for n,
we need to show it is also true for n+1.
…
Conclusion: SUM= 2n for any n>=1.
12
1. Correctness: Induction
More examples on showing the partial
correctness of algorithms using induction:
■ Euclid’s GCD algorithm (pp.103-104)
■ outputtree(T) (pp.105)
■ McCarthy’s 91 algorithm (pp.106)
■ The algorithm for moving the Towers of Hanoi
(exercise!)
13
1. Correctness: Assertions
Induction can also be used to show the correctness of
large algorithms.
■ A human is difficult to visualize the entire operations of a
large algorithm.
■ So, the remedy is to use modules, as we do for
designing algorithms.
■ The independence among modules is of prime
important.
■ In this way, it is usually possible to conclude the
correctness of whole algorithm from that of each
module.
14
1. Correctness: Assertions
The specifications of each module consist of two
parts, or two assertions:
■ Pre-conditions: permissible input upon which the
module is expected to operate.
■ Post-conditions: the desired effect of the module on
input data.
■ These two conditions describe two computation states.
■ In practice, more assertions can be added in the middle
of a module, especially at some key points.
15
1. Correctness: Assertions
Example 2: Given a box of various multicoloured
balls, calculate the maximum number of balls
which have a matching color.
The corresponding algorithm is a little complex,
so the five assertions added are helpful to
showing the correctness (pp.108-110).
16
1. Correctness: Termination
■ To get total correctness, we need to show termination
for any partially correct algorithm.
■ However, there exists no mechanical method of
deciding whether an algorithm halts.
■ So, as proving partial correctness, showing termination
may also require creativity in many cases.
■ The basic idea to show why a loop or recursion must
terminate is to observe that this computation will
gradually become simpler.
■ Usually, this means that some value will continuously
decrease (or increase) as the loop or recursion is
executed every time.
17
1. Correctness: Termination
Example 3: Why the algorithm for Ackermann’s function
A will terminate for any input pair (x, y)?
module A(x, y)
{Compute Ackermann’s function on any input (x, y), which
are non-negative integers}
if x=0
then answer is y+1
else if y=0
then answer is A(x-1,1)
else answer is A(x-1,A(x,y-1))
endmodule
18
2. Nonprocedural Algorithms
Procedural Algorithms:
■ Define an algorithm as a set of basic operations
controlled by sequence, selection, and iteration.
■ Namely, an algorithm is viewed as a procedure to be
followed in order to carry out a task.
■ Two features of this procedural definition:
- It defines what operations the processor needs to do;
- It specifies the order in which these operations are to
be executed.
19
2. Nonprocedural Algorithms
■ Procedural definition of algorithms has some
deficiencies.
■ So some alternative definitions have been proposed.
- Functional (or applicative) programming, derived from
Church’s lambda calculus.
- Logic programming, derived from predicate calculus.
20
Summary
This Lecture:
■ Correctness
■ Nonprocedural algorithms
Next Lectures:
- Computer Architecture
21