random.mlw 2.29 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
(** {1 Pseudo-random generators}
3 4 5 6 7

   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

MARCHE Claude's avatar
MARCHE Claude committed
8
      [val random_int: unit -> {} int {}]
9

MARCHE Claude's avatar
MARCHE Claude committed
10
   is typically enough. Two calls to [random_int] return values that can not
11 12 13 14
   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
15
   explicit (module [State]) or global (module [Random]). Functions [init] allow
16
   to reset the generators according to a given seed.
MARCHE Claude's avatar
MARCHE Claude committed
17

18 19
 *)

MARCHE Claude's avatar
MARCHE Claude committed
20
(** {2 Purely applicative generators} *)
21 22 23 24 25 26 27 28

theory Generator

  use import bool.Bool
  use import int.Int

  type generator

Andrei Paskevich's avatar
Andrei Paskevich committed
29
  function create int : generator
30

Andrei Paskevich's avatar
Andrei Paskevich committed
31
  function next generator : generator
32

Andrei Paskevich's avatar
Andrei Paskevich committed
33
  function get_bool generator : bool
34

Andrei Paskevich's avatar
Andrei Paskevich committed
35
  function get_int  generator int : int
36 37 38 39 40 41 42

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

end

MARCHE Claude's avatar
MARCHE Claude committed
43 44 45
(** {2 Mutable states of pseudo-random generators}

  Basically a reference containing a pure generator. *)
46 47 48 49 50 51

module State

  use import int.Int
  use export Generator

52
  type state model { mutable state: generator }
53

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

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

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

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

66 67 68 69 70
  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 }
71 72 73

end

MARCHE Claude's avatar
MARCHE Claude committed
74
(** {2 A global pseudo-random generator} *)
75 76 77 78

module Random

  use import int.Int
79
  use import State
80

81
  val s: state
82

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

85
  let self_init () = self_init s
86

87 88 89 90
  let random_bool ()
    ensures { s.state = next (old s.state) }
    ensures { result = get_bool s.state }
  = random_bool s
91

92 93 94 95 96 97
  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
98 99

end