Algorithms are problem solving
recipes intended for humans; they are usually expressed in a mixture
of natural language, mathematical notation, and programming notation.
In contrast, programs are intended for machine execution; they are
expressed in a programming language.
How do we go from a correct algorithm to a correct program?
The background for my lectures is the experience with LEDA, CGAL, and
EXACUS, three algorithm library projects I was involved with.
In the first main part, I discuss certifying algorithms. Certifying
algorithms return not only the value they are supposed to compute but
also a witness (certificate) which allows the user of the algorithm to
convince itself of the correctness of the value returned. I give
of certifying algorithms and discuss the limits of certification.
In the second main part, I discuss the implementation of geometric
algorithms. Their implementation is particularly difficult, because
geometric algorithms are usually designed for inputs in general
position and for the Real-RAM model of computation. I give examples,
miserably naive implementations can fail, show how to realize
a Real-RAM as needed for computational geometry, discuss approaches to
the general position problem, and finally come to exact algorithms for
The background for my lectures is the experience with building the
systems LEDA, CGAL and EXACUS.
I recommend that you read through the
slides of the talk on LEDA.
- The Implementation of
Most algorithms of computational geometry are designed for inputs in
general position (no three points on a line, no three lines
intersecting, ...) and for the Real-RAM model of computation. However,
actual inputs are not necessarily in general position and floating
point arithmetic is a coarse approximation of real arithmetic.
- <>The exact computation paradigm: I then discuss the specific
problem of computing Arrangement
of Conics in the plane. I discuss an exact and complete algorithm
which can cope with all inputs. The algorithm implements a Real-RAM as
needed for this problem.
On an input x, a certifying algorithm
for a function f does not only return y, the alleged function value
f(x), but also a certificate (proof, convincing evidence) of the
equality ``y = f(x)''. In this way, a user of the program can convince
himself that the program worked correctly on the given input x. We
advocate certifying programs as a pragmatic approach to program
Algorithms: this is a survey paper on certifying algorithms. It is
still under construction.
Priority Queues is a short paper which discusses how to check the
correctness of priority queues. It appeared in SODA 99.
Prof. Dr. Kurt
Algorithms and Complexity