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 JAA25749; Wed, 17 Jul 2002 09:15:07 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA25725 for ; Wed, 17 Jul 2002 09:15:06 +0200 (MET DST) Received: from mel-rto3.wanadoo.fr (smtp-out-3.wanadoo.fr [193.252.19.233]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g6H7F6f02119 for ; Wed, 17 Jul 2002 09:15:06 +0200 (MET DST) Received: from mel-rta7.wanadoo.fr (193.252.19.61) by mel-rto3.wanadoo.fr (6.5.007) id 3D1848E600BFD1CC; Wed, 17 Jul 2002 09:14:26 +0200 Received: from AlphaSystem.dnsalias.net (80.11.74.121) by mel-rta7.wanadoo.fr (6.5.007) id 3D2A78FA003F3F75; Wed, 17 Jul 2002 09:14:26 +0200 Received: from localhost ([127.0.0.1] helo=alphasystem.dnsalias.net) by AlphaSystem.dnsalias.net with esmtp (Exim 3.36 #1 (Debian)) id 17Uj0z-000MGu-00; Wed, 17 Jul 2002 09:14:25 +0200 From: "Johan Baltié" To: Jacques Garrigue CC: caml-list@inria.fr Subject: Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) Date: Wed, 17 Jul 2002 08:14:24 +0100 Message-Id: <20020717071424.M65430@wanadoo.fr> In-Reply-To: <20020717154649S.garrigue@kurims.kyoto-u.ac.jp> References: <20020717061954.M92611@wanadoo.fr> <20020717154649S.garrigue@kurims.kyoto-u.ac.jp> X-Mailer: Open WebMail 1.61 20020204 X-OriginatingIP: 192.6.2.192 (baltie_j) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > From: "Johan Baltié" > > > Well, Ada does. The strong typing gives information to the compiler for it to > > deduce when range checking is not needed: > > > > declare > > subtype Index is Integer range 1..10; > > type Arr is array (Index) of Integer; > > a : Arr; > > element : Integer; > > j : Index := 1; > > k : Integer := 11; > > begin > > for i in a'Range loop > > element := a(i); -- no range checking needed, i is in range by definition > > end loop; > > a(j); -- range checking not needed, j is within Index by definition > > a(k); -- range checking needed due possibility of k being outside of Index > > exception > > when Constraint_Error => > > -- process the out-of-range error from a(k) > > end; > > This is similar to Pascal ranges. > The trouble is that typical code doesn't look like that, but rather > > let bubble_once arr = > for i = 0 to Array.length arr - 2 do > if arr.(i) > arr.(i+1) then begin > let tmp = arr.(i) in > arr.(i) <- arr.(i+1); > arr.(i+1) <- tmp > end > done > > or worse > > let bubble_one arr last = > assert (last < Array.length arr); > let swap i = > let tmp = arr.(i) in > arr.(i) <- arr.(i+1); > arr.(i+1) <- tmp > in > for i = 0 to last - 1 do > if arr.(i) < arr.(i+1) then swap i > done > > In the first case, that's not too difficult: you just have to know > that Array.length returns the length of an array, and do a bit of > arithmetic. > > In the second case, you should propagate the information from the > assertion to the loop bound, and additionally treat swap as if it were > inlined (we know it is its only call context). No it's not such a mess. A subrange is a type. As ocaml is a bit strong on is types it solves itself the problem let bubble_one arr last = assert (last < Array.length arr); let swap i = let tmp = arr.(i) in arr.(i) <- arr.(i+1); arr.(i+1) <- tmp in for i = 0 to last - 1 do if arr.(i) < arr.(i+1) then swap i done the {..} are my subranges types bubble_one: a' {0..b'} array -> int -> unit swap: {0..b'} -> unit the "for" should be like in Ada, working with range types and no problem will ever occur. > And it's fragile: > if you move "swap" out of the function, then it might be used on any > array, and you have to do the bound check. If you move swap out of the function, in another one using another array, the type will change and a warning/error/check will occur if the types are incompatible. > [snipped] > Jacques Garrigue Ciao Jo ------------------- 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