Pseudo-random generators

This easiest way to get random numbers (of random values of any type) is to take advantage of the non-determinism of Hoare triples. Simply declaring a function

[val random_int: unit -> {} int {}]

is typically enough. Two calls to [random_int] return values that can not be proved equal, which is exactly what we need.

The following modules provide slightly more: pseudo-random generators which are deterministic according to a state. The state is either explicit (module [State]) or global (module [Random]). Functions [init] allow to reset the generators according to a given seed.

Mutable states of pseudo-random generators

Basically a reference containing a pure generator.

module State

  use int.Int

  type state = private mutable { }

  val create (seed: int) : state

  val init (s: state) (seed: int) : unit writes {s}

  val self_init (s: state) : unit writes {s}

  val random_bool (s: state) : bool writes {s}

  val random_int (s: state) (n: int) : int writes {s}
    requires { 0 < n }
    ensures  { 0 <= result < n }

end

A global pseudo-random generator

module Random

  use int.Int
  use State

  val s: state

  let init (seed: int) = init s seed

  let self_init () = self_init s

  let random_bool ()
  = random_bool s

  let random_int (n: int)
    requires { 0 < n }
    ensures  { 0 <= result < n }
  = random_int s n

end