( A really interesting post on static elimination of array bounds checking by Oleg...)
Some questions and suggestions: What is the relation to the sized types by Lars Pareto and John Hughes? What is the relation to classical range analyses for (e.g.) array index expressions, which have been known for a long time for imperative languages? A program analysis like range analysis is not exact, of course: it must make safe approximations sometimes and will sometimes say that an array index might be out of bounds when it actually won't. In your framework, this seems to correspond to the fact that you must verify your propositions about index expressions. If the formulae fall into some decidable category, then they can be verified automatically, otherwise an automatic method based on your framework will have to give up sometimes, just like a conventional program analysis. The formulae you give in your example are all Presburger formulae, for which there are decision procedures, and you could use a public domain Presburger solver like the Omega Test by Bill Pugh. Have you though of this possibility? Björn Lisper _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell