3 ms·

No, the proof is the proof that you generate with formal methods. Is exhaustive testing even possible in theory?

• ffsm8 2y ago
  Not just in theory but actually done: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html
  • impossiblefork 2y ago
    I don't agree that that's exhaustive testing. Full branch test coverage etc., is normal and sensible and it's great, but that's very different from having a proof that given certain preconditions, you will have certain postconditions.
    • ffsm8 2y ago
      100% branch coverage means that you've fundamentally covered all potential states your software can enter. What you're asking for is literally only possible in theory and entirely pointless in the context of reality, because you cannot guarantee that a device is available at runtime, invalidating any proof. The same applies to any engineering projects, software or otherwise
      • akiarie 2y ago
        Not even remotely. if (x > 0) { /* code */ } else { /* more code */ } Branch coverage just means that all the lines above are executed in some test. That's fundamentally different from dealing with all the different values that `x` could take on at run time.
        • ffsm8 2y ago
          You're missing the point. Given your example no software can ever handle this equation given infinite numbers, as all CPUs have a maximum number they can compare. Just like you cannot prove that a bridge will be able to handle a given load. Engineering fundamentally can only make assurances within expectations. Your tests define these expectations, and by covering 100% branching coverage you've exhaustively explored all valid states your software can have. Do note I'm talking about actual 100% branching coverage here, not just 100% coverage of your own code, ignoring libraries and runtimes you've imported. That's way harder then you seem to think and the reason why sqlite (the linked page) has so much more testing code then application code
      • ratmice 2y ago
        I agree with the other commenter that his is not even remotely true... given something like loop { if (A) { ... } if (B) { ... } } 100% branch coverage means you've encountered both cases, but the loop could have encountered these in any number of ways specifically this branch could be encountered as either A && B both A && !B && B && !A, all of them exhaustively, and could even depend upon whether the order branches were taken matters. While formal methods give an exhaustive proof.
      • SassyBird 2y ago
        > 100% branch coverage means that you've fundamentally covered all potential states your software can enter. No, it doesn’t. bool is_even(int n) { return true; } bool test_is_even() { return is_even(2); } 100% test coverage. And yet.
        • ffsm8 2y ago
          Are you seriously that big brain that you think that's smart? Your example software makes the claim that integers that the given runtime/interpreter/VM can handle will be assured as true. This was tested. Nobody said that any description of the software is always correct, just because a test was added that tests random stuff Also note that that's not 100% coverage. It merely covers your code, which builds upon other code. Feel free to actually read the given link. Your horizon might be expanded. Or don't, and keep your dunning kruger worldview
          • discreteevent 2y ago
            Those who dunning kruger should be careful lest they be dunning krugered themselves!
            • ffsm8 2y ago
              I guess we're desperate to get to answer to the question of how dumb comment chains on this forum can get, and wherever everyone involved is either mentally or actually in the /r/im-12-and-this-is-smart phase.