random.mlw 2.46 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 52 53

module State

  use import int.Int
  use export Generator

  type state model {| mutable state: generator |}

Andrei Paskevich's avatar
Andrei Paskevich committed
54
  val create (seed: int) :
55 56
    {} state { result.state = create seed }

Andrei Paskevich's avatar
Andrei Paskevich committed
57
  val init (s: state) (seed: int) :
58 59
    {} unit writes s { s.state = create seed }

Andrei Paskevich's avatar
Andrei Paskevich committed
60
  val self_init (s: state) :
61 62
    {} unit writes s {}

Andrei Paskevich's avatar
Andrei Paskevich committed
63
  val random_bool (s: state) :
64 65
    {}
    bool writes s
Andrei Paskevich's avatar
Andrei Paskevich committed
66
    { s.state = next (old s.state) /\ result = get_bool s.state }
67

Andrei Paskevich's avatar
Andrei Paskevich committed
68
  val random_int (s: state) (n: int) :
69 70
    { 0 < n }
    int writes s
Andrei Paskevich's avatar
Andrei Paskevich committed
71
    { s.state = next (old s.state) /\ result = get_int s.state n /\
72 73 74 75
      0 <= result < n }

end

MARCHE Claude's avatar
MARCHE Claude committed
76
(** {2 A global pseudo-random generator} *)
77 78 79 80 81 82

module Random

  use import int.Int
  use import module State

Andrei Paskevich's avatar
Andrei Paskevich committed
83
  val s: state
84 85 86 87 88 89 90 91 92 93

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

  let self_init () =
    {} self_init s {}

  let random_bool () =
    {}
    random_bool s
Andrei Paskevich's avatar
Andrei Paskevich committed
94
    { s.state = next (old s.state) /\ result = get_bool s.state }
95 96 97 98

  let random_int (n: int) =
    { 0 < n }
    random_int s n
Andrei Paskevich's avatar
Andrei Paskevich committed
99
    { s.state = next (old s.state) /\ result = get_int s.state n /\
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
      0 <= result < n }

end

module Test

  use import module Random

  let test1 () =
    init 42;
    let x = random_int 10 in
    init 42;
    let y = random_int 10 in
    assert { x = y }

end

MARCHE Claude's avatar
MARCHE Claude committed
117
(***
118 119 120 121
Local Variables:
compile-command: "unset LANG; make -C .. modules/random"
End:
*)