Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

library: simplified module Random

parent 3fc6c7b8
......@@ -292,26 +292,19 @@ module State63
use import int.Int
use import Int63
use export random.Generator
type state = abstract { mutable state: generator }
type state = private mutable { }
val create (seed: int63) : state
ensures { result.state = create seed }
val init (s: state) (seed: int63) : 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_int63 (s: state) (n: int63) : int63 writes {s}
requires { 0 < n }
ensures { s.state = next (old s.state) }
ensures { result = get_int s.state n }
ensures { 0 <= result < n }
end
......@@ -326,7 +319,7 @@ module Random63
val s: state
let init (seed: int63) ensures { s.state = create seed } = init s seed
let init (seed: int63) = init s seed
let self_init () = self_init s
......
......@@ -17,29 +17,6 @@
*)
(** {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. *)
......@@ -47,26 +24,19 @@ end
module State
use import int.Int
use export Generator
type state = abstract { mutable state: generator }
type state = private mutable { }
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
......@@ -80,19 +50,15 @@ module Random
val s: state
let init (seed: int) ensures { s.state = create seed } = init s seed
let init (seed: int) = 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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment