From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA27096; Sun, 14 Jul 2002 15:17:06 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA27093 for ; Sun, 14 Jul 2002 15:17:05 +0200 (MET DST) X-SPAM-Warning: Sending machine is listed in blackholes.five-ten-sg.com Received: from athlon.baretta.com (r-mi214-6a72.tin.it [62.211.4.72]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g6EDH3f24916 for ; Sun, 14 Jul 2002 15:17:04 +0200 (MET DST) Received: from baretta.com (localhost.localdomain [127.0.0.1]) by athlon.baretta.com (Postfix) with ESMTP id C4AD72724F for ; Sun, 14 Jul 2002 15:24:00 +0200 (CEST) Message-ID: <3D317B70.4010605@baretta.com> Date: Sun, 14 Jul 2002 15:24:00 +0200 From: Alessandro Baretta Organization: Baretta srl -- www.baretta.com User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020529 X-Accept-Language: it, en MIME-Version: 1.0 To: Ocaml Subject: Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) References: <200207081952.PAA28813@hickory.cc.columbia.edu> <15657.61603.221054.289184@spike.artisan.com> <200207090442.AAA05638@hickory.cc.columbia.edu> <001f01c2271e$8037adf0$d100a8c0@warp> <3D2C5B77.6060303@ozemail.com.au> <200207102229.g6AMTKB22278@orchestra.cs.caltech.edu> <3D2ECE7F.5040108@ozemail.com.au> <20020714142540.A4150@gogol.zorgol> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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