Good one! I'll keep it in mind.

One of the simplest incorrect algorithms uses the assertion that x^2 + x + 41 is prime for non-negative integer x, which works for many integers x (from 0 all the way up to 39), then fails for most (but not all) integers after that.

I am not quite sure whether we are on the same wavelength, but I don't like to say "Incorrect algorithm that outputs a correct answer for a good number of test cases". I prefer to say : "incomplete algorithm".

My example would be as follows:

Suppose we seek the roots of a second order equation "A*X^2 + B*X+C", let us suppose that X is not specified to a particular set (it can be either Real or Complex). If we suppose that "A" and "B" are both different than zero, then if Delta = B^2 + 4*A*C < 0, then there would be two possibilities : either two complex roots, or no roots.

I found this situation quite interesting : It would be incorrect to say that that equation have two complex roots if "X" is in R. And the opposite is also correct (to say there are no solution while X is in C). Each set have different way of thinking.

Not quite true; since all real numbers are also complex numbers, we know that if A, B, C are any complex numbers, then there are exactly 2 solutions when A is nonzero (which may be the same if the quadratic expression is a constant multiple of a perfect square), and in every case when either A or B is nonzero or when C is zero, there is at least one solution (not always a real number solution)

@Christopher : I guess you did not get what I wanted to say.

It is correct to say that every Real number is Complex. Is it correct to say : when A is different from 0, and when Delta is negative, then we have two solutions ?

The problem lies in the origin of X : does X belong to the real numbers or CAN be complex. The latter isn't always verified for all kind of problems.

Yes that is correct (when the coefficients are real; otherise delta is likely not real and cannot always be compared to 0) - in any case, there are always two complex solutions, but there may not be any real solutions - sorry I misunderstood

@Christopher : You know? You gave me a new very useful argument.

Thank you very much.

A folklore example is swapping the value of two (integer) references without using a local variables. Take a programming language with call-by-reference and the following function:

swap(&int a, &int b) {

a := a - b; // value of a is a0 - b0

b := a + b; // value of b is a0 - b0 + b0 = a0

a := b - a; // value of a is a0 - a0 + b0

}

Assume the value of a is a pointer to the value a0 and b to b0. Then after a call to swap(a, b) the value pointed to by a and b are swapped ... except if a and b both point to the same memory address, in which case they point to the value 0.

This is more an example of the problems related to reasonning about programs in the presence of pointers but I think that it qualifies as an example of tricky algorithm.

@Silvano

Yeah, that's an interesting example I ran into back when I was learning C, but it's not exactly very relevant for my presentation on formal verification.

Thanks for the contribution, though. If I ever extend the formalities I'm working with to include pointer-related axioms, I'll remember it!

i think you should model any algorithm so, by using transition relations and CTL rules you can define non functional specification results. that mean each proposition that TRUE in your model can be FALSE in Correct model

by this way you can use to each example for you conditions

Would the following post be useful for you?

http://googleresearch.blogspot.com.br/2006/06/extra-extra-read-all-about-it-nearly.html

Great example, thanks!

There are too many easy ways to make these algorithms "trip", and this blog post covers it nicely.

Hoare specifically treats computer arithmetics differently from classic arithmetics in his axiomatic basis, and some people completely forget about it when proving algorithms 'informally'.

I think the folklore example (of silvano dal zilio)

may have problems with large numbers

the way i first saw that folklore example was with no arithmetic,

and therefore no possibility of overflow

a := a xor b;

b := b xor a; /* now b is what a was */

a := a xor b; /* now a is what b was */

Take any optimization problem that is known to have a poly-time algorithm for a simpler case and then generalize it, you will gain a very large subset of instance for which it should work, then many that will fail.

Great example: Fractional Knapsack's greedy algorithm

then try using the same greedy algorithm but instead use it on 0-1 Knapsack. You can come up with some really nasty counterexamples but it still works for some.

Fabricio, I can give you a good one from NUMBER THEORY.

The FERMAT PRIMALITY TEST is as follows:

For every Prime Number, a^(p) = a (mod p). See:

http://en.wikipedia.org/wiki/Fermat%27s_little_theorem

Now, this theorem is NOT true both ways. In other words, although for every prime this theorem MUST hold, the reverse is not true. CARMICHAEL NUMBERS pass the primality test, so, they TRICK the test ! See:

http://en.wikipedia.org/wiki/Carmichael_numbers

So, If you wrote a PRIMALITY VERIFICATION program to verify whether a number is prime or not by literally writing 30, 50 lines of code to check whether a^p is equal to a MOD p, your code would be correct 99+ percent of the time, except, for a very small set of numbers that are CARMICHAEL numbers, it would be tricked. This is because, CARMICHAEL numbers are pseudo-primes (almost primes, but can be factored, thereby cheating the Fermat test).

Hope this helps ... Tolga

My comment is more of informing than an example (as I already provided one):

@Tolga, you described a theorem that has a straightforward algorithm as a corollary, though I agree with your point, but the theorem itself is not an algorithm much as a program isn't an algorithm but can be encoded to describe an algorithm (it is a test but is not described in a systematic procedure). The beauty of such theorems are the fact you can use it in an algorithm. Many algorithms use that test by Fermat but it is severely out of date with respect to cryptography and computational complexity theory with respect to computational number theory. Subtle, but important and something I normally have to distinguish carefully for even my colleagues (not just students).

If you were to formulate it as an algorithm (inputs, outputs, procedure, problem instance, etc...) it is a good example of an pretty old technique that works sometimes but fails for many. Good job Tolga!

@Daniel, sure. This is a very simple example. But, it proves a point: Imagine if this test was being used in a much larger program, and since there was a mistake in handling it (like I described above), the entire program was "messing up" as described by Fabricio in his question ... But, not all the time. Almost in an "intermittent" manner ... However, what looks intermittent is actually very deterministic ... There is a very clear way, why it fails ... This is an example of a LOGICAL ERROR that the programmer made. Another example of an intermittent error is MEMORY FAULTs. One bit flips, and, all hell brakes loose. ECC only protects you so far ...

The problem that Fabricio described is "using input test vectors and looking at the result" and if, for a huge portion of the time the answer is correct, calling it "CORRECT." There was a very active research area of "AUTOMATIC TEST PATTERN GENERATION" and I don't know its current status, but, the idea is this: when I have an "n" bit input, there are a total of 2^n input vectors I have to test to say that, "this works correctly 100% of the time". If I go below 2^n, I am definitely below 100%. The problem is that, when I have 64 or 128bit inputs, applying every input test vector is intractable. Something's gotta give ! So, I try to come up with all sorts of rules on how a portion of the input vectors are not necessary, since they are SUBSUMED by others ... I try to boil it down to 100 or 200. If all 200 tests pass, I can say that, I am 99.9999% correct ! good enough. It's CORRECT ... But, NOT 100% !!!

If you remember the INTEL Pentium bug, which made INTEL recall millions of Pentium chips, it passed every verification test ! but, it failed 0.0000001% of the time. I guess, that was bad enough !