examples/array_of_list.mlw

   1
   2 (** Turning a list into an array.
   3
   4   This is a small program to illustrate the use of Why3's Peano
   5   numbers (see module mach.peano.Peano).
   6
   7   It turns a list into an array. The point is that we use machine
   8   integers (for the list length and for array indices) but we avoid
   9   having to prove the absence of arithmetic overflow.
  10
  11   Author: Jean-Christophe Filliâtre (CNRS)
  12 *)
  13
  14 use int.Int
  15 use option.Option
  16 use list.List
  17 use seq.Seq
  18 use mach.peano.Peano
  19 use mach.peano.Int63
  20 use mach.int.Int63
  21 use mach.array.Array63 as A
  22 use list.NthLength
  23
  24 (** The length of a list computed with Peano numbers. *)
  25 let rec length (l: list 'a) : Peano.t
  26   variant { l } ensures { result = length l }
  27 = match l with
  28   | Nil      -> Peano.zero
  29   | Cons _ l -> Peano.succ (length l)
  30   end
  31
  32 (** To turn a list into an array, we first compute the length of the
  33     list with the function above, then we build an array of that size,
  34     and finally we fill it with the elements from the list.
  35
  36     Note: `Array.make` requires a value of type 'a, so the code below
  37     requires a non-empty list. (In OCaml, we would return the empty
  38     array [||] when the list is empty, but there is no such empty
  39     array in Why3's library.)
  40 *)
  41 let partial array_of_list (l: list 'a) : (a: A.array 'a)
  42   requires { l <> Nil }
  43   ensures  { A.length a = length l }
  44   ensures  { forall i. 0 <= i < length l -> Some a[i] = nth i l }
  45 = let n = to_int63 (length l) in
  46   match l with Nil -> absurd | Cons x ll ->
  47   let a = A.make n x in
  48   let rec fill (i: int63) (ll: list 'a) : unit
  49     requires { i >= 1 && n - i = length ll }
  50     requires { forall j. 0 <= j < i -> Some a[j] = nth j l }
  51     requires { forall j. i <= j < n -> nth (j-i) ll = nth j l }
  52     variant  { n - i }
  53     ensures  { forall j. 0 <= j < n -> Some a[j] = nth j l }
  54   = match ll with Nil -> ()
  55     | Cons x ll -> A.(a[i] <- x); fill (i+1) ll
  56     end in
  57   fill 1 ll;
  58   return a
  59   end