(** {1 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. *) (** {2 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 (** {2 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 (** {2 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