bench/check-ce/array_poly.mlw

   1
   2 module A
   3
   4   use int.Int
   5   use array.Array
   6
   7   let f1 (a:array int) : int
   8   = a[0]
   9
  10   let f2 (a:array int) : unit
  11     requires { a.length >= 2 }
  12     ensures { a[0] <> a[1] }
  13   = a[0] <- 42
  14
  15 end
  16
  17 module B
  18
  19   use int.Int
  20   use array.Array
  21   clone array.Sorted with
  22     type elt=int,
  23     predicate le=(<=)
  24
  25
  26   let f1 (a:array int) : unit
  27     ensures { sorted a }
  28   = ()
  29
  30
  31   let f2 (a:array int) : array int
  32     ensures { sorted result }
  33   = a
  34
  35 end