Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] productivity improvement
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2002-07-15 (08:23)
From: Xavier Leroy <xavier.leroy@i...>
Subject: Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)
> 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.

Well, for this purpose, array index expressions must be restricted to
a sub-language where inequations between index expressions are
decidable.  A well-known such sub-language is Presburger arithmetic:
index expressions are variables, constants, and sums and products of
expressions.  I don't know of any significantly more expressive
sub-language that has the required decidability properties.

> 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.

Obligatory preliminary remark: the cost of run-time array bound checks
is not that high, since on modern processors it is performed
largely in parallel with the actual array access.  On my tests,
ocamlopt -unsafe is at best 25% faster than ocamlopt on array
intensive programs.

This said, the approach you outline was investigated in depth by
Hongwei Xi in his work on Dependent ML:

It's an interesting reading.

- Xavier Leroy
To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: