16 ms·
Proponents of this approach would probably argue that non-linear arithmetic doesn't show up frequently in index computation. I don't know whether this is true o
by munin 9y ago
Proponents of this approach would probably argue that non-linear arithmetic doesn't show up frequently in index computation. I don't know whether this is true or not, would be curious to see data. Based on my own experience I'd agree with it, with caveats for things like a[i%a.length] but you could probably do something there like replace % with an approximation that is linear and sound.
- seanwilson 9y agoEven if it was infrequent (I'd be interested in data too!), what do you do when it does come up? It's very difficult to constrain yourself to decidable domains when you want to write arbitrary programs and capture arbitrary program properties. You could let the proof goal go through without a proof but you'd have to replace it with a runtime check otherwise if the goal happened to be false all your static guarantees are out of the window (like doing a bad type cast in C++ for instance).