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  10345 reads

Browse archivesActive forum topics 
Recent comments
4 days 20 hours ago
4 days 21 hours ago
5 days 20 hours ago
6 days 8 hours ago
6 days 14 hours ago
6 days 14 hours ago
6 days 14 hours ago
6 days 17 hours ago
6 days 17 hours ago
6 days 18 hours ago