4 ms·
> The problem of array overflow/underflow is undecidable in the general case. Obviously. > Various verification techniques (like SMT solvers) can only prove s
by catnaroek 11y ago
> The problem of array overflow/underflow is undecidable in the general case.
Obviously.
> Various verification techniques (like SMT solvers) can only prove some usages, but not all.
Turns out this is good enough for most cases. Verifying 80% of your array index manipulations is better than verifying none of it.
- armitron 11y agoWhere do you get "good enough for most cases" or the 80% from? Let's see the hard facts rather than conjecture masquerading as such. My personal experience points to opposite results of what you claim.
- ant6n 11y ago> My personal experience points to opposite results of what you claim. Let's see the hard facts rather than conjecture masquerading as such.
- catnaroek 11y agoMy main use cases for manipulating indices directly are: (0) Implementing lexical contexts and environments whose variables are identified with de Bruijn indices or levels. (1) Implementing multidimensional arrays and operations on them (e.g., matrix multiplication). In both of these cases, a solver for the theory of integer arithmetic can check that I'm using my indices right.