new library for random generators

modules/random.mlw

+
+(* 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
+
+      parameter 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
+
+  logic create int : generator
+
+  logic next generator : generator
+
+  logic get_bool generator : bool
+
+  logic 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 |}
+
+  parameter create (seed: int) :
+    {} state { result.state = create seed }
+
+  parameter init (s: state) (seed: int) :
+    {} unit writes s { s.state = create seed }
+
+  parameter self_init (s: state) :
+    {} unit writes s {}
+
+  parameter random_bool (s: state) :
+    {}
+    bool writes s
+    { s.state = next (old s.state) and result = get_bool s.state }
+
+  parameter random_int (s: state) (n: int) :
+    { 0 < n }
+    int writes s
+    { s.state = next (old s.state) and result = get_int s.state n and
+      0 <= result < n }
+
+end
+
+(* A global pseudo-random generator. *)
+
+module Random
+
+  use import int.Int
+  use import module State
+
+  parameter s: state
+
+  let init (seed: int) =
+    {} init s seed { s.state = create seed }
+
+  let self_init () =
+    {} self_init s {}
+
+  let random_bool () =
+    {}
+    random_bool s
+    { s.state = next (old s.state) and result = get_bool s.state }
+
+  let random_int (n: int) =
+    { 0 < n }
+    random_int s n
+    { s.state = next (old s.state) and result = get_int s.state n and
+      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
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C .. modules/random"
+End:
+*)