Browse thread
Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)
-
Johan Baltié
-
Jacques Garrigue
- Johan Baltié
-
Jacques Garrigue
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Johan Baltié <johan.baltie@w...> |
| Subject: | Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) |
> 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