It can be used in static analysis or type checking. E.g.
reply if (x >= 0) {
x += 10
if (x =< 9) {
// unreachable
}
}
initial: [-oo, oo]
x >= 0 : [0, oo]
x += 10: [10, oo]
x =< 9 : [10, 9] (empty)I’m working on a static analyser at the moment that does this, and the inferences that can be made just from the information of intervals is quite impressive.
One thing you run into pretty quickly though in a lot of languages is integer overflow ruining your day - in your example above the commented section is reachable for signed ints that support overflow and that adds a whole other layer of complexity to things.
replyWe recently implemented this idea in an LLVM optimisation pass based on value-range information from sensor datasheets [1].
replyIn physics, whenever you make a measurement it has a precision. Usually you represent this as a normal distribution, but for calculations it can be easier to represent this as an interval.
replyThe police measure the distance my car travelled [ 99.9, 100.1 ] m and the time it took [ 3.3, 3.4 ] s - how fast was my car going? [29.38, 30.33] m/s according to the interval calculator.
Physics students learn exactly this method before they move on to more sophisticated analysis with error distributions.
And one might want to approximate error distribution calculus with a method that will look like the one here
replyIt’s astonishing how nobody hasn’t mentioned abstract interpretation yet. Under classical static analysis, if you can “prove” that a variable does not have values in some unsound zones, you can e.g. “prove” soundness or apply further optimizations.
replyThe interval abstract domain works under interval analysis with an algebra that’s the same of this calculator. It’s funny to implement something like that on source/binary level :)