h2g2 The Hitchhiker's Guide to the Galaxy: Earth Edition

http://www.h2g2.com/A514379

What it means for a computer program to be correct
How you can prove that a program is correct.

I'm particularly proud of the non-technical example...

Comments, criticisms, typos, nitpicks, all very much welcome.

I guess this is a candidate for the sin bin because it doesn't feature the A........ number in the forum's title. In short, it lacks Forum Correctness

doh!
seconded

Interesting article.

The example you gave of a partially correct program might need revision.

The program would either buy a winning ticket and be finished, or keep buying new tickets until you are totally broke. Instead of leading from [i am poor] to [i am rich] it leads to [i am broke]and will stop because there is no more money left to buy lottery tickets for.
What you were looking for is a program that would keep going ad infinitum until it could end.

~^M^~

other thread is at http://www.h2g2.com/F48874?thread=99642 ....

I spotted a number of things with the article, and with the forums about it, so here goes.
When you look up the different possible user inputs in a program, and it isn't in the list, it is called an exception. Trapping this out and having a sensible response is called exception reporting. There is a practical problem with the three programs on three computers, etc. The problem is that typically, if you are an american firm doing it, then all three of your programming teams will probably be americans, and so they will ALL have the same logical blind spots. And will promptly all fall over them.
Performance monitors and profilers are different, as they are for checking efficiency. However, you can use GPROF (under unix) to output to a file, which you can then analyse to see how much of your program is being checked by your current set of tests.
There is a name for the problem of programs terminating, it is called "the halting problem", and has the problem that you can not prove that any given program will halt given arbitrary input. The most you can prove is under what circumstances the program will halt.
This is where efficiency profilers come in. They can help you make sure that your tests give you full code coverage, but only in conjuction with another program that analyses their output.
There are programs out there that can prove correctness, but as far as I know, the only work for monotonic reasoning (where it goes from 1 provably correct statement to another provably correct statement) using horne clauses (where whatever the condition, it only proves 1 fact) on closed world databases (like the bus timetable, if it isn't on the timetable, you know that you can't catch a bus, because there isn't one). Unfortunately, most problems don't fit into these very narrow catagories, and thus you cannot use theorem proving programs to construct your code.
Phew, wasn't that a bit long winded. still, when you start talking logic, it tends to get a bit that way.

Editorial Note: This conversation has been moved from 'Peer Review Sin Bin' to 'Program Correctness'.

Back to Entry - this became Edited Entry A563807 Program Correctness