User loginNavigation 
Using real arithmetic to eliminate bounds checking?The usual problem with eliminating array bounds checking is that integer arithmetic is undecidable. For example, the compiler can't figure out that you can index into an array of m·n elements using an expression like i·n+j, even if it's known statically that 0≤i<m and 0≤j<n. Or rather, that particular problem is simple, but it's hard to come up with a general algorithm that would work for many different programs. Many people are trying to use dependent types and machinecheckable proofs for that, like in Hongwei Xi's paper. It just occurred to me that statements like "if i âˆˆ [0,m1] and j âˆˆ [0,n1], then i·n+j âˆˆ [0,m·n1]" (all segments are closed) can be interpreted and proved in real arithmetic, instead of integer arithmetic. The nice thing is that real arithmetic is decidable. If that approach works, we can have a language with integerparameterized types like "array of n elements" and "integer between m and n", and have a simple definition of what the type checker can and cannot automatically prove about programs using such types, without having to write any proofs explicitly. Of course the system will be limited by the fact that it's talking about reals rather than integers. For example, there will be problems with integerspecific operations on type parameters, like division and remainder, but I don't know how often these will be required. Are there any obvious problems with this idea? Has it been tried? By Vladimir Slepnev at 20140513 14:25  LtU Forum  previous forum topic  next forum topic  other blogs  9666 reads

Browse archives
Active forum topics 
Recent comments
2 weeks 3 days ago
3 weeks 3 days ago
5 weeks 5 days ago
6 weeks 3 days ago
6 weeks 3 days ago
6 weeks 6 days ago
6 weeks 6 days ago
7 weeks 8 hours ago
7 weeks 21 hours ago
7 weeks 1 day ago