From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 7FAF4BBBB for ; Mon, 4 Sep 2006 03:03:38 +0200 (CEST) Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8413VVw011210 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Mon, 4 Sep 2006 03:03:37 +0200 Received: (qmail 29257 invoked by uid 107); 4 Sep 2006 01:03:18 -0000 Received: from vwmetnet.metnet.navy.mil (192.16.167.21) by selenite.metnet.navy.mil with SMTP; 4 Sep 2006 01:03:18 -0000 Received: from Adric.metnet.fnmoc.navy.mil ([10.100.105.102]) by vwmetnet.metnet.navy.mil (NAVGW 2.5.2.9) with SMTP id M2006090401160517817 for ; Mon, 04 Sep 2006 01:16:05 GMT Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id 9A553AC00; Sun, 3 Sep 2006 18:00:02 -0700 (PDT) To: caml-list@inria.fr Subject: Eliminating array bounds check Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20060904010002.9A553AC00@Adric.metnet.fnmoc.navy.mil> Date: Sun, 3 Sep 2006 18:00:02 -0700 (PDT) X-Miltered: at concorde with ID 44FB7B63.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; oleg:01 abbreviation:01 abstraction:01 run-time:01 avoided:01 ocaml:01 oleg:01 pldi:01 ocaml:01 annotations:01 mutable:01 arrays:01 recursion:01 mutable:01 arrays:01 On Aug 31, John Skaller wrote: > Typing is always an abbreviation (abstraction) and sometimes > stronger or weaker than desired: for example array bounds > checks at run time, because the type system doesn't cope > with array sizes as part of the type. Although that is true that making the type system track the size of a (dynamically allocated) array is too much of a hassle, array bounds checks at run-time can be entirely and safely avoided, in OCaml as it is. For example: http://pobox.com/~oleg/ftp/ML/eliminating-array-bound-check-literally.ml shows how to implement the bsearch (the standard Dependent ML example from the famous Xi and Pfenning's PLDI98 paper) in the current OCaml. The above code has exactly the same number of checks as the DML code; there are no array bound checks -- and yet the code has the same static assurances of the absence of out-of-bounds array access errors. The code (given at the end of that file) even looks quite like the original DML code (quoted at the beginning of that file), only without any type annotations. A more interesting example is the textbook KMP string search, which uses mutable arrays, general recursion, and creative index expressions (with mutable arrays storing array indices). http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html (well, the referenced code is actually in Haskell, but it is easy to re-write it in OCaml; I can do that if called to). The above page points to the PLPV talk that contains formalization and the proof method (as well some proofs in Twelf). Briefly, we rely on the type system to propagate assurances made in a small `security kernel' through the rest of the code. The security kernel does have to be verified. Our examples show that the kernel is far simpler than the rest of the code: the KMP kernel, for example, is made of non-recursive functions performing additions and subtraction of integers.