(no subject)

[Horst von Brand]

Martin Dalecki <[e-mail]> said:

[...]

> Goedel tells you about axiomatic systems which encompass both ARITHMETIC
> and RECURSION.
> And dman there is still the inifity requirement it needs... (int is
> usually at best 64 bit!)

Checking each possible combination of, say, 10 variables @ 64 bits each is
certianly finite, but that is not very practical.

> This means Goedels Unvollstaendigkeitheorem is about theories, where all
> the definitions can be expressed by a formalization "roughly" equivalent
> to the Turing-machines (Please don't take me by word: This is just an
> "explanation for dummies"). [...]

Not Goedel's theorem, Turing's proof of the existence of noncomputable
functions is relevant here. Both are essentially the same, anyway.

> [...] The whole theorem is compleatly
> irrelevant here, since one dosn't need to find an universal tester for
> overflows in arrays of all programms but just a prober for all the
> programms one will feed it.

Can't be done, unless you _severely_ restrict the programs considered
(where the severity depens on the resources you are able to bring to the
task). Sure, you can restrict the programs by style guidelines, prohibiting
use of certain functions, etc. If a smart enough program can't show it
doesn't have problems, probably a smart human can't either, and it's time
to rewrite/redesign. Now the problem is: How smart is "smart enough"? What
exact types of checks should the program consider? How do we make sure no
possibly dangerous construct slips through? The last question leads back
to the question of how to characterize all possibly dangerous constructions
in C. And AFAIKS there is very little that can't be abused there. Then we
are back at the problem with lint and lclint and its ilk: No reasonable way
to make them shut up for perfectly reasonable code. Hundreds of false
negatives for each positive just don't make an useful tool.

> And in practical cases in CAN BE PROVEN THAT PROGRAMMS DON'T CONTAIN 
> POSSIBLE OVERFLOWS. Like in the following example:
> 
> int main(int argc, char *argv[] )
> {
> 	return 0;
> }

Very practical program, that one.
-- 
Dr. Horst H. von Brand                       mailto:[e-mail]
Departamento de Informatica                     Fono: [phone]
Universidad Tecnica Federico Santa Maria              [phone]
Casilla 110-V, Valparaiso, Chile                Fax:  [phone]