random.mlw 2.29 KB
 Jean-Christophe Filliatre committed Jun 21, 2011 1 `````` `````` MARCHE Claude committed May 07, 2012 2 ``````(** {1 Pseudo-random generators} `````` Jean-Christophe Filliatre committed Jun 21, 2011 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 committed May 07, 2012 8 `````` [val random_int: unit -> {} int {}] `````` Jean-Christophe Filliatre committed Jun 21, 2011 9 `````` `````` MARCHE Claude committed May 07, 2012 10 `````` is typically enough. Two calls to [random_int] return values that can not `````` Jean-Christophe Filliatre committed Jun 21, 2011 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 `````` Guillaume Melquiond committed May 09, 2012 15 `````` explicit (module [State]) or global (module [Random]). Functions [init] allow `````` Jean-Christophe Filliatre committed Jun 21, 2011 16 `````` to reset the generators according to a given seed. `````` MARCHE Claude committed May 07, 2012 17 `````` `````` Jean-Christophe Filliatre committed Jun 21, 2011 18 19 `````` *) `````` MARCHE Claude committed May 07, 2012 20 ``````(** {2 Purely applicative generators} *) `````` Jean-Christophe Filliatre committed Jun 21, 2011 21 22 23 24 25 26 27 28 `````` theory Generator use import bool.Bool use import int.Int type generator `````` Andrei Paskevich committed Jun 29, 2011 29 `````` function create int : generator `````` Jean-Christophe Filliatre committed Jun 21, 2011 30 `````` `````` Andrei Paskevich committed Jun 29, 2011 31 `````` function next generator : generator `````` Jean-Christophe Filliatre committed Jun 21, 2011 32 `````` `````` Andrei Paskevich committed Jun 29, 2011 33 `````` function get_bool generator : bool `````` Jean-Christophe Filliatre committed Jun 21, 2011 34 `````` `````` Andrei Paskevich committed Jun 29, 2011 35 `````` function get_int generator int : int `````` Jean-Christophe Filliatre committed Jun 21, 2011 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 committed May 07, 2012 43 44 45 ``````(** {2 Mutable states of pseudo-random generators} Basically a reference containing a pure generator. *) `````` Jean-Christophe Filliatre committed Jun 21, 2011 46 47 48 49 50 51 `````` module State use import int.Int use export Generator `````` Andrei Paskevich committed Oct 13, 2012 52 `````` type state model { mutable state: generator } `````` Jean-Christophe Filliatre committed Jun 21, 2011 53 `````` `````` Andrei Paskevich committed Oct 13, 2012 54 55 `````` val create (seed: int) : state ensures { result.state = create seed } `````` Jean-Christophe Filliatre committed Jun 21, 2011 56 `````` `````` Andrei Paskevich committed Oct 13, 2012 57 58 `````` val init (s: state) (seed: int) : unit writes {s} ensures { s.state = create seed } `````` Jean-Christophe Filliatre committed Jun 21, 2011 59 `````` `````` Andrei Paskevich committed Oct 13, 2012 60 `````` val self_init (s: state) : unit writes {s} `````` Jean-Christophe Filliatre committed Jun 21, 2011 61 `````` `````` Andrei Paskevich committed Oct 13, 2012 62 63 64 `````` val random_bool (s: state) : bool writes {s} ensures { s.state = next (old s.state) } ensures { result = get_bool s.state } `````` Jean-Christophe Filliatre committed Jun 21, 2011 65 `````` `````` Andrei Paskevich committed Oct 13, 2012 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 } `````` Jean-Christophe Filliatre committed Jun 21, 2011 71 72 73 `````` end `````` MARCHE Claude committed May 07, 2012 74 ``````(** {2 A global pseudo-random generator} *) `````` Jean-Christophe Filliatre committed Jun 21, 2011 75 76 77 78 `````` module Random use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 79 `````` use import State `````` Jean-Christophe Filliatre committed Jun 21, 2011 80 `````` `````` Andrei Paskevich committed Jul 01, 2011 81 `````` val s: state `````` Jean-Christophe Filliatre committed Jun 21, 2011 82 `````` `````` Andrei Paskevich committed Oct 13, 2012 83 `````` let init (seed: int) ensures { s.state = create seed } = init s seed `````` Jean-Christophe Filliatre committed Jun 21, 2011 84 `````` `````` Andrei Paskevich committed Oct 13, 2012 85 `````` let self_init () = self_init s `````` Jean-Christophe Filliatre committed Jun 21, 2011 86 `````` `````` Andrei Paskevich committed Oct 13, 2012 87 88 89 90 `````` let random_bool () ensures { s.state = next (old s.state) } ensures { result = get_bool s.state } = random_bool s `````` Jean-Christophe Filliatre committed Jun 21, 2011 91 `````` `````` Andrei Paskevich committed Oct 13, 2012 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 `````` Jean-Christophe Filliatre committed Jun 21, 2011 98 99 `````` end``````