3 ms·

>Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. fo

>Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. for any input space in which a finite number of checks has greater than literally 0% (measure zero) of being representative this problem is trivial (finite space).

Sharlin 9y ago
Trivial in the math sense. Not trivial in the real-world programming sense. Very different things.
- tikhonj 9y ago
  This is an important point: even a finite search space quickly gets out of hand in practical terms. I've worked a bit on bounded verification which comes down to comparing loop-free programs with finite inputs for equality. It is not easy in practice! Modern approaches use sophisticated proof search algorithms (ie SMT solvers) and still struggle to scale beyond relatively small and simple programs. I don't know the numbers off-hand because verification was not the bottleneck in my application, but I suspect that even sophisticated modern methods scale poorly beyond a few hundred instructions or for large inputs (ie algorithms with complex behavior over arrays). If you have a function that takes a single 32-bit floating point input and runs in, say, 100 cycles, you can test all the possible inputs in a couple minutes or so. If you have multiple floats as inputs or the function is more complex, you can exhaustively check it with an SMT solver or the like. If your function depends on hundreds or thousands of inputs and has complex looping logic, you probably can't exhaustively check it with any automated solution. Real programs, of course, are orders of magnitude more complex than even the last example. Verifying them automatically is effectively impossible even if they have finite inputs, guaranteed bounds on loops and are "trivial" in the mathematical sense.

Sharlin 9y ago

Trivial in the math sense. Not trivial in the real-world programming sense. Very different things.

tikhonj 9y ago
This is an important point: even a finite search space quickly gets out of hand in practical terms. I've worked a bit on bounded verification which comes down to comparing loop-free programs with finite inputs for equality. It is not easy in practice! Modern approaches use sophisticated proof search algorithms (ie SMT solvers) and still struggle to scale beyond relatively small and simple programs. I don't know the numbers off-hand because verification was not the bottleneck in my application, but I suspect that even sophisticated modern methods scale poorly beyond a few hundred instructions or for large inputs (ie algorithms with complex behavior over arrays). If you have a function that takes a single 32-bit floating point input and runs in, say, 100 cycles, you can test all the possible inputs in a couple minutes or so. If you have multiple floats as inputs or the function is more complex, you can exhaustively check it with an SMT solver or the like. If your function depends on hundreds or thousands of inputs and has complex looping logic, you probably can't exhaustively check it with any automated solution. Real programs, of course, are orders of magnitude more complex than even the last example. Verifying them automatically is effectively impossible even if they have finite inputs, guaranteed bounds on loops and are "trivial" in the mathematical sense.