Speaker: David Faitelson, Afeka Tel Aviv Academic College of Engineering
Title: Conjectures and Refutations of Computer Programs
Abstract
How
can we know that a program is correct? this is a basic and fundamental
question that faces every programmer. Yet even though the theory of
program correctness is well understood, in practice it has had little
effect on programmers. Indeed, most programmers are even ignorant of its
existence. This is unfortunate because as we all know only too well,
software today is as buggy as it ever was.
An essential ingredient of the traditional approach to
program correctness is the concept of proof. However proof is a
double-edged sword. On the one hand it is powerful, as those that use it
to write programs, consistently produce high quality code that is
orders of magnitude more reliable than traditional code. But on the
other hand it requires a great deal of mathematical sophistication and
rote work. Attempts to automate proof have not solved this problem. As
we all know proof cannot be completely automated. Thus when an automatic
theorem prover fails, we don't know if this is because the theorem is
wrong or because the prover is not powerful enough. Another argument
against proof is that while it is essential for the development of the
theories that are used by all traditional engineers, no engineer is
expected to derive proofs as part of his or her job.
I would like to have my cake and eat it too. I would
like to keep most of the power of the proof based approach but to avoid
the need to actually perform the proofs. In order to do that I am
willing to leave the high ground of absolute mathematical certainty and
descend into the lower (but still effective) plane of scientific
knowledge as it was defined by the philosopher Karl Popper. Briefly,
Popper argued that we can never be certain that a scientific theory is
correct, we can only refute it by showing an example in which its
predictions are wrong. A theory is good according to Popper if it offers
a way to refute itself. According to this point of view the assertions
that we provide in an attempt to prove a program, form an excellent
theory because it is easy to refute by finding an assignment of state
variables that falsifies the assertions.
In the last year I have been developing Refute --- a
system for generating high quality algorithmic programs --- and
recently it has reached a point where it is possible to use it to
construct non trivial algorithms.
The essential idea of refute is to find bugs, not in
the program but in the program's proof of correctness. Thus, the
engineer writes the assertions that he believes show why the program is
correct and the system tries to refute his assertions by looking for
counter-examples that demonstrate why it is wrong. Of course, if the
system doesn't find any counter-examples we cannot deduce that the
program is correct, but under some reasonable assumptions we can
increase our confidence in the program's correctness.
Refute consists of a language, an analyser and a
compiler. The language combines the imperative language described by
Dijkstra in his book "a method of programming" (but extended to support
procedures, dynamic allocation and records) with the relational
language of the Alloy analyzer. In addition, the language includes
constructs for specifying preconditions, postconditions and loop
invariants. These constructs define a proof of correctness for each
procedure, namely that if the parameters of the procedure satisfy the
precondition then the procedure's body will terminate and satisfy its
postcondition. The analyzer is a fully automatic tool that checks the
proof by verifying that it holds in a finite scope. If it doesn't, the
analyser displays a counter-example. The compiler translates the
language into a variety of popular programming languages including C,
C++, Java and C#.
In this talk I will demonstrate Refute and argue why
the particular approach that I have chosen is more effective than
existing systems that share a similar purpose.
