Why3 Standard Library index



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.


Purely applicative generators

theory Generator

  use import bool.Bool
  use import int.Int

  type generator

  function create int : generator

  function next generator : generator

  function get_bool generator : bool

  function get_int  generator int : int

  axiom get_int_def:
    forall g: generator, n : int.
    0 < n -> 0 <= get_int g n < n

end

Mutable states of pseudo-random generators

Basically a reference containing a pure generator.

module State

  use import int.Int
  use export Generator

  type state model { mutable state: generator }

  val create (seed: int) : state
    ensures { result.state = create seed }

  val init (s: state) (seed: int) : unit writes {s}
    ensures { s.state = create seed }

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

  val random_bool (s: state) : bool writes {s}
    ensures { s.state = next (old s.state) }
    ensures { result = get_bool s.state }

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

end

A global pseudo-random generator

module Random

  use import int.Int
  use import State

  val s: state

  let init (seed: int) ensures { s.state = create seed } = init s seed

  let self_init () = self_init s

  let random_bool ()
    ensures { s.state = next (old s.state) }
    ensures { result = get_bool s.state }
  = random_bool s

  let random_int (n: int)
    requires { 0 < n }
    ensures  { s.state = next (old s.state) }
    ensures  { result = get_int s.state n }
    ensures  { 0 <= result < n }
  = random_int s n

end

Generated by why3doc 0.87.3