Implementing Algorithms
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
examples
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,
how
miserably naive implementations can fail, show how to realize
a Real-RAM as needed for computational geometry, discuss approaches to
overcome
the general position problem, and finally come to exact algorithms for
curves
and surfaces.
-
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
Geometric Algorithms
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
correctness.
- Certifying
Algorithms: this is a survey paper on certifying algorithms. It is
still under construction.
- Checking
Priority Queues is a short paper which discusses how to check the
correctness of priority queues. It appeared in SODA 99.
Prof. Dr. Kurt
Mehlhorn
Max-Planck-Institut für
Informatik
Algorithms and Complexity
Group (AG1)
Im Stadtwald
66123
Saarbrücken
Germany