stdlib/random.mlw

   1
   2 (** {1 Pseudo-random generators}
   3
   4    This easiest way to get random numbers (of random values of any type)
   5    is to take advantage of the non-determinism of Hoare triples.
   6    Simply declaring a function
   7
   8       [val random_int: unit -> {} int {}]
   9
  10    is typically enough. Two calls to [random_int] return values that can not
  11    be proved equal, which is exactly what we need.
  12
  13    The following modules provide slightly more: pseudo-random generators
  14    which are deterministic according to a state. The state is either
  15    explicit (module [State]) or global (module [Random]). Functions [init] allow
  16    to reset the generators according to a given seed.
  17
  18  *)
  19
  20 (** {2 Mutable states of pseudo-random generators}
  21
  22   Basically a reference containing a pure generator. *)
  23
  24 module State
  25
  26   use int.Int
  27
  28   type state = private mutable { }
  29
  30   val create (seed: int) : state
  31
  32   val init (s: state) (seed: int) : unit writes {s}
  33
  34   val self_init (s: state) : unit writes {s}
  35
  36   val random_bool (s: state) : bool writes {s}
  37
  38   val random_int (s: state) (n: int) : int writes {s}
  39     requires { 0 < n }
  40     ensures  { 0 <= result < n }
  41
  42 end
  43
  44 (** {2 A global pseudo-random generator} *)
  45
  46 module Random
  47
  48   use int.Int
  49   use State
  50
  51   val s: state
  52
  53   let init (seed: int) = init s seed
  54
  55   let self_init () = self_init s
  56
  57   let random_bool ()
  58   = random_bool s
  59
  60   let random_int (n: int)
  61     requires { 0 < n }
  62     ensures  { 0 <= result < n }
  63   = random_int s n
  64
  65 end