A software correctness proof?

bsilbaugh · 2012-03-03 16:13:56

The context: I currently work in the area of scientific computing, which is another way of saying that I have a strong background in numerical methods (and physics) but my understanding of software development is largely based on personal experience and the information I can gleam from online forums, articles, and books. The "software" I develop performs physics based modeling of fluid and structural dynamics (basically solves differential equations using Finite Volume Methods). The software runs on both shared and distributed memory systems (I mostly rely on MPI for this).

The question: Suppose you are given a piece of software (the source code for stand-alone program or library). Is there a theory, or well founded method, you could use to conclude that software is free of any programming errors? That is, something beyond ad-hoc tests which only check necessary conditions for correctness.

My amateur hypothesis: My inclination is to conclude that one could only prove correctness in simple cases. For more complicated algorithms (e.g. solving differential equations) one can only run "spot checks" for a handful of representative cases and then optimistically infer that it will most-likely work for all other cases. Perhaps I'm missing something?

(EDIT: cleaned up some typos)

Last edited by bsilbaugh (2012-03-03 16:26:56)

karol · 2012-03-03 16:26:16

I only know that Dijkstra had something to do with it: http://en.wikipedia.org/wiki/Edsger_W._Dijkstra

wikipedia wrote:

From the 1970s, Dijkstra's chief interest was formal verification. The prevailing opinion at the time was that one should first write a program and then provide a mathematical proof of correctness. Dijkstra objected noting that the resulting proofs are long and cumbersome, and that the proof gives no insight on how the program was developed. An alternative method is program derivation, to "develop proof and program hand in hand". One starts with a mathematical specification of what a program is supposed to do and applies mathematical transformations to the specification until it is turned into a program that can be executed. The resulting program is then known to be correct by construction. Much of Dijkstra's later work concerns ways to streamline mathematical argument.

I have no idea if his work came into fruition.

Xyne · 2012-03-03 16:30:15

The ability to prove correctness depends on the language. Functional languages seem to be much more adapted for this, and I regularly come across papers and discussions about proving correctness when I work with Haskell. This may be true for other functional languages too, but there seems to be a greater number of academic computer scientists and mathematicians in the Haskell community. They tend to publish peer-reviewed articles about such issues in Haskell, something which I rarely if ever see for other languages.

There are some good points and references given here:
http://stackoverflow.com/questions/4077 … s-properti

The number one thing that you'll often hear from functional programming afficionados is that Haskell is referentially transparent, which makes it easy to do things like reason about programs, and write correctness proofs of programs. Writing a correctness proof of a C program (or even an Objective CaML program) ranges from difficult to effectively impossible - the presence of side effects in the code is very hard to cope with in formal reasoning, and when programs get beyond trivial simplicity, they rapidly become intractable for proofs.

Source: http://scienceblogs.com/goodmath/2006/1 … askell.php

/dev/zero · 2012-03-03 20:09:13

bsilbaugh wrote:

The question: Suppose you are given a piece of software (the source code for stand-alone program or library). Is there a theory, or well founded method, you could use to conclude that software is free of any programming errors? That is, something beyond ad-hoc tests which only check necessary conditions for correctness.

Surely if it compiles, that means the code is free of programming errors. That is, doesn't error-free compilation imply syntactic correctness according to the language's grammar?

To do more than this, I think would require defining what additional measures you have in mind for assessing correctness. As you probably know even better than I do, numerical approximations always comes with error, even when using the correct algorithm. If you want to check that the programmer used the best algorithm known to the existing literature, I think that would require a manual check - although I suspect you didn't quite mean this.

bsilbaugh · 2012-03-03 21:49:39

/dev/zero wrote:

bsilbaugh wrote:
The question: Suppose you are given a piece of software (the source code for stand-alone program or library). Is there a theory, or well founded method, you could use to conclude that software is free of any programming errors? That is, something beyond ad-hoc tests which only check necessary conditions for correctness.
Surely if it compiles, that means the code is free of programming errors. That is, doesn't error-free compilation imply syntactic correctness according to the language's grammar?
To do more than this, I think would require defining what additional measures you have in mind for assessing correctness. As you probably know even better than I do, numerical approximations always comes with error, even when using the correct algorithm. If you want to check that the programmer used the best algorithm known to the existing literature, I think that would require a manual check - although I suspect you didn't quite mean this.

I suppose I should have been a little more clear about what I mean about "programming errors". By "programming errors", I mean that the compiled code executes the algorithm that the developer believes he/she implemented. Whether or not the developer chose the correct algorithm to begin with is another matter, and outside the intended scope of my original post. Perhaps "programmer error" would have been a better choice of words. Another term frequently used to describe what I mean is software "verification" (as opposed to "validation").

For example, suppose a programmer implements the following C function which compiles under gcc 4.6:

// A function for computing centered finite differences
void derivative(int n, double x[], double f[], double dfdx[]){
        int i;
        for(i=0; i<n; ++i);
             dfdx[i] = (f[i+1] - f[i-1])/(x[i+1] - x[i-1]);
}

This implementation gives amazing run-time performance Nonetheless, it's obviously not what the programmer intended, as the for loop does nothing (other than increment i). In this particular case, the error could be caught by a simple unit test or careful eye. But, sometimes the errors are even more insidious and yet compile. I'll see if I can dig up a better example of some of the stupid errors I've come across (including my own work--sadly), that would make sense to a more general audience.

Obviously, following good programming practices goes a long way to avoiding such errors. But, it would seem that even the best of the best still screw up now and then.

Last edited by bsilbaugh (2012-03-03 22:03:11)

bsilbaugh · 2012-03-03 22:27:01

Thanks karol and Xyne. Those are some interesting leads.

Blµb · 2012-03-04 10:57:09

Take a look at Hoare Calculus and Annotation Calculus
One of the books we used in a lecture I attended about formal software verification was "The Science of Programming" by David Gries, this one seems to contain the Annotation Calculus (couldn't find any good links on the web right now).
I'll check if I still have the list of recommended books for the lecture.

EDIT:
I just remembered: did you know about cbmc?
It probably still lacks features you need for your software. (Back when I had to use it it had several problems, like it couldn't handle initializers properly, so I had to write "int a; a = x" rather than "int a = x;", also, it didn't do float/integer conversions properly. Actually I don't even know if it did floating point arithmetic at all properly...)
(Might be a bit tricky to install, it needs a SAT solver, like minisat)

Last edited by Blµb (2012-03-04 12:39:55)

lunar · 2012-03-04 16:08:49

@bsilbaugh: You can proof the correctness of a program with methods specifically targeted to the program whose correctness is to be prooven, but this is tedious, cumbersome and requires a lot of theoretical knowledge about formal methods and software verification. You can also proof the presence or absence of certain error classes, e.g. numeric stability of concrete implementations of numerical algorithms, array access within array bounds, race conditions in multithreaded programs, etc. For some combinations of error classes and target languages there are even ready-to-use tools. In some high-level languages such as Haskell or Prolog, where referential transparency and purity of all expressions (or a subset thereof) is guaranteed, you can sometimes also apply standard mathematical methods like induction proofs.

However, there is no general method to proof the correctness of an arbitrary program, because the question whether a program halts at a specific state ("common halting problem"), and related to this also the question whether a program can reach a specific (potentially errorneous) state, is proven to be "undecidable", which means that there cannot be a simple algorithm that answers this question with "yes" or "no".

tomegun · 2012-03-04 19:38:42

/dev/zero wrote:

bsilbaugh wrote:
The question: Suppose you are given a piece of software (the source code for stand-alone program or library). Is there a theory, or well founded method, you could use to conclude that software is free of any programming errors? That is, something beyond ad-hoc tests which only check necessary conditions for correctness.
Surely if it compiles, that means the code is free of programming errors. That is, doesn't error-free compilation imply syntactic correctness according to the language's grammar?
To do more than this, I think would require defining what additional measures you have in mind for assessing correctness. As you probably know even better than I do, numerical approximations always comes with error, even when using the correct algorithm. If you want to check that the programmer used the best algorithm known to the existing literature, I think that would require a manual check - although I suspect you didn't quite mean this.

Syntactic correctness is not enough. Things you would want to prove is

That your program is well defined (in C syntactic correct programs can perform undefined operations (hence segfaults))
That your program terminates
That your program is (contextually) equivalent to another program. Typically you do this if you have a simple, but inefficient program and you want to make sure that an optimized, but complicated version behaves the same.

In general these problems cannot be solved (look up the Halting problem), but in specific cases they can (and one might make an argument that in the cases where you cannot prove things about your program, maybe you'd be better off not using it at all ;-) )

tomegun · 2012-03-04 19:51:04

bsilbaugh wrote:

/dev/zero wrote:
bsilbaugh wrote:
The question: Suppose you are given a piece of software (the source code for stand-alone program or library). Is there a theory, or well founded method, you could use to conclude that software is free of any programming errors? That is, something beyond ad-hoc tests which only check necessary conditions for correctness.
Surely if it compiles, that means the code is free of programming errors. That is, doesn't error-free compilation imply syntactic correctness according to the language's grammar?
To do more than this, I think would require defining what additional measures you have in mind for assessing correctness. As you probably know even better than I do, numerical approximations always comes with error, even when using the correct algorithm. If you want to check that the programmer used the best algorithm known to the existing literature, I think that would require a manual check - although I suspect you didn't quite mean this.
I suppose I should have been a little more clear about what I mean about "programming errors". By "programming errors", I mean that the compiled code executes the algorithm that the developer believes he/she implemented. Whether or not the developer chose the correct algorithm to begin with is another matter, and outside the intended scope of my original post. Perhaps "programmer error" would have been a better choice of words. Another term frequently used to describe what I mean is software "verification" (as opposed to "validation").
For example, suppose a programmer implements the following C function which compiles under gcc 4.6:
// A function for computing centered finite differences
void derivative(int n, double x[], double f[], double dfdx[]){
        int i;
        for(i=0; i<n; ++i);
             dfdx[i] = (f[i+1] - f[i-1])/(x[i+1] - x[i-1]);
}
This implementation gives amazing run-time performance Nonetheless, it's obviously not what the programmer intended, as the for loop does nothing (other than increment i). In this particular case, the error could be caught by a simple unit test or careful eye. But, sometimes the errors are even more insidious and yet compile. I'll see if I can dig up a better example of some of the stupid errors I've come across (including my own work--sadly), that would make sense to a more general audience.
Obviously, following good programming practices goes a long way to avoiding such errors. But, it would seem that even the best of the best still screw up now and then.

There are static analyzers that will try to find common errors (use after free, infinite loops etc). Coverity is one such tool often used on the kernel.

If what you want is formal verification, then you basically are forced to choose a language which lends itself to be verified (and for which integration with formal tools exist). C is a non-starter for this. As mentioned by others, Haskell is probably your best bet at something that can be verified, is relatively widespread and whose performance is reasonable (though if you chose C for performance reasons, Haskell might not work for you, it depends on your usecase).

goulo · 2012-03-04 20:32:24

See http://en.wikipedia.org/wiki/Formal_verification for more info/links.

I took some courses about formal software verification (i.e. mathematically proving a program's correctness) long ago, for functional languages and for procedural languages. You can easily use such techniques for simple stuff (e.g. proving that an implementation of a stack is correct). E.g. Boyer and Moore's research:

http://www.cs.utexas.edu/~moore/best-id … index.html

As you suggest in the OP, it indeed quickly becomes more messy/difficult for nontrivial programs.

Arch Linux

#1 2012-03-03 16:13:56

A software correctness proof?

#2 2012-03-03 16:26:16

Re: A software correctness proof?

#3 2012-03-03 16:30:15

Re: A software correctness proof?

#4 2012-03-03 20:09:13

Re: A software correctness proof?

#5 2012-03-03 21:49:39

Re: A software correctness proof?

#6 2012-03-03 22:27:01

Re: A software correctness proof?

#7 2012-03-04 10:57:09

Re: A software correctness proof?

#8 2012-03-04 16:08:49

Re: A software correctness proof?

#9 2012-03-04 19:38:42

Re: A software correctness proof?

#10 2012-03-04 19:51:04

Re: A software correctness proof?

#11 2012-03-04 20:32:24

Re: A software correctness proof?

Board footer