search

rdebath / Brainfuck

Brainfuck torture test. Brainfuck interpreters and compilers to C, V. VIM syntax file for brainf*ck. Fast JIT Assembly, JIT C running, Perl, Python, php, Ruby, lua, go, awk, neko, PS1, bash, ook, trollscript etc etc
GNU General Public License v2.0
201 stars 22 forks source link

Is there any integrity test of an implementation of brainfuck? #2

Closed clarkzjw closed 9 years ago

clarkzjw commented 9 years ago

Well, I have seen many brainfuck examples in your repos, but I'm curious that is there any test can be found to test whether an implementation of brainfuck is correct?

For example, we can say brainfuck or python is Turing-complete language. But can we say an brainfuck interpreter is complete after some kind of tests?

rdebath commented 9 years ago

The test for "Turing completeness" is a mathematical test, so a proof can be made to ensure that a particular language definition is equivalent to other languages that are defined as Turing complete.

But the same cannot be done for a real implementation of a language because the theoretical concept of a Turing machine contains "Infinite storage", which no physical machine has. Nevertheless, in theory, it is possible to prove that a program follows the specification of the language with the exception that the memory won't actually be infinite.

This can be done in the same mathematical manner that the Turing completeness of the language is done, but most people find this rather problematical.

The way it normally boils down to is testing ... If you have a set of tests that checks every possible code path it's a simple step from there to proving that the program is correct for all cases. You will notice that this depends on a set of test cases for your individual implementation, which may not be the same as any other one ever invented.

Still, for the Brainfuck specification and an implementation as simple as my "Micro BF" a full set of tests is quite possible and for a small number of cells is probably covered by bitwidth.b, in part because I have specifically tried to add tests to this script every time I've encountered a bug in any interpreter. Extending this to the actual number of cells available in the interpreter would either need a test for every cell to be created or some inductive rules to say cell K+1 is the same as cell K where K<N, so again it's probably possible.

But even with an implementation only a little more complex, for example Deadbeef the number of possible paths starts getting very large and a proof of correctness becomes VERY difficult.

clarkzjw commented 9 years ago

Thank you for your explanation.