3 ms·
> In a binary search, each variable can be zero, one, some(*), max, overflowed. The combination of these is not infinite as the values of some that cause differ
by rileymat2 2y ago
> In a binary search, each variable can be zero, one, some(*), max, overflowed. The combination of these is not infinite as the values of some that cause different behavior is much more reasonable when grouped into chunks of the same behavior.
You are presuming that the algorithm is correct in the first place. Contrived example.
binary_search(array, key) {
if (key == 453) explode_world()
//Do correct binary search.
}
So you also need to prove explode_world is not called or something similar but less contrived is not in there.
- adrianN 2y agoThat is easily caught by a model checker that tries the equivalence classes. Or just normal coverage tooling.
- joshka 2y agoNo. I'm presuming that you're able to look at the branches in code and write white box tests. Here the relevant two branches are 453 and anything other than 453. For addition of unsigned numbers, the relevant branches are 0 + 0, 0 + 1, 0 + max, 1 + 0 (usually can be skipped), 1 + 1, 1 + max (which overflows), etc. The number of relevant material states is bounded and knowable. It's neither unbounded (1,2,3,4,5,6 ... ) or unknowable as the algorithm is available.