Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Alessandro Baretta <alex@baretta.com>]

Berke Durak wrote:
> On Fri, Jul 12, 2002 at 10:41:35PM +1000, John Max Skaller wrote:
> [...]
> 
> Hey, wait a minute, how do you plan to statically detect bounds exceptions ?
> It's as undecidable as detecting infinite recursions.
> 
> 	let rec f () =
> 	   let a = [|1;2|] in
>        if compiler_is_gonna_say_that_there_is_gonna_be_a_bounds_error f then
>           a.(0)
>        else
>           a.(3)

If the compiler attempted to catch at least the most evident 
  bounds errors, it would very simply detect that your code 
contains an expression which, if evaluated, would raise a 
runtime bounds error. Hence, the compiler should simply 
reject the code. Of course, in the absence of some unusual 
limitation on the expressive power of array creation and 
indexing expression, the general problem of static detection 
of array indexing errors is undecidable.

I wonder if the compiler gurus at the INRIA know what kinds 
of constraints imposed on the language would allow the 
compiler to statically check array indexing. I can imagine a 
few applications, such as signal analysis, where the program 
logic is simple enough that such a restricted language might 
suffice, and come to the aid of the developer who presently 
uses unsafe arrays for the sake of speed, but with no help 
from the compiler at prooving that the program is correct 
with respect to array indexing.

I have a feeling that most applications which would benefit 
from static checking of array indexing boil down to finite 
state automata. I'm pretty sure that a language based of 
FSAs could do static bounds checking.

Alex

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners