3 ms·

Formal methods aren't "testing". As you say, though, exhaustive testing is sometimes possible.

bluGill 2y ago
It is normally safe to assume the exhaustive testing isn't possible because the total states to exhaustively tests exceeds the number of atoms in the universe. There are a few exceptions, but in general we should assume it is always impossible to exhaustively test programs. Which means we need to use something else to find what the limits are and test only those, or use formal methods (both would be my recommendation - though I'll admit I have yet to figure out how to use formal methods)
- dllthomas 2y ago
  > in general we should assume it is always impossible to exhaustively test programs The whole program? Yes. For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
  - mananaysiempre 2y ago
    Brute forcing a single 32-bit input has also been usefully performed in some cases, such as for single-precision implementations of special functions[1]. [1] https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
    - bluGill 2y ago
      32 bits is a bit over 4 billion states, so that is doable. However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
      - dllthomas 2y ago
        > 32 bits is a bit over 4 billion states, so that is doable. Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally. > However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable. I'm pretty confident we're all in agreement there.
Retr0id 2y ago
I agree that it's not testing in the strict sense, but fuzzing isn't really testing either. The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)
- NovemberWhiskey 2y ago
  This seems to neglect the fundamental difference between static and dynamic analysis. Formal methods approaches don’t usually need me to run my code.
- _flux 2y ago
  I guess I need to disagree :). Why isn't fuzzing testing? Ultimately it ends up running the code and seeing if it works—for some definition of "working", that is, it doesn't crash—even if it may pick the ways it chooses the input by considering how the code behaves while running it. Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
  - dllthomas 2y ago
    I think fuzzing is doing testing, but often using other techniques (including sometimes formal methods) to improve the effectiveness of that testing.

It is normally safe to assume the exhaustive testing isn't possible because the total states to exhaustively tests exceeds the number of atoms in the universe. There are a few exceptions, but in general we should assume it is always impossible to exhaustively test programs. Which means we need to use something else to find what the limits are and test only those, or use formal methods (both would be my recommendation - though I'll admit I have yet to figure out how to use formal methods)

dllthomas 2y ago
> in general we should assume it is always impossible to exhaustively test programs The whole program? Yes. For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
- mananaysiempre 2y ago
  Brute forcing a single 32-bit input has also been usefully performed in some cases, such as for single-precision implementations of special functions[1]. [1] https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
  - bluGill 2y ago
    32 bits is a bit over 4 billion states, so that is doable. However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
    - dllthomas 2y ago
      > 32 bits is a bit over 4 billion states, so that is doable. Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally. > However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable. I'm pretty confident we're all in agreement there.

Retr0id 2y ago

I agree that it's not testing in the strict sense, but fuzzing isn't really testing either. The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)

NovemberWhiskey 2y ago
This seems to neglect the fundamental difference between static and dynamic analysis. Formal methods approaches don’t usually need me to run my code.
_flux 2y ago
I guess I need to disagree :). Why isn't fuzzing testing? Ultimately it ends up running the code and seeing if it works—for some definition of "working", that is, it doesn't crash—even if it may pick the ways it chooses the input by considering how the code behaves while running it. Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
- dllthomas 2y ago
  I think fuzzing is doing testing, but often using other techniques (including sometimes formal methods) to improve the effectiveness of that testing.