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

["Johan Baltié" <johan.baltie@wanadoo.fr>]

> From: "Johan Baltié" <johan.baltie@wanadoo.fr>
> 
> > 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