MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

random.mlw 2.47 KB
 Jean-Christophe Filliâtre committed Jun 21, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 `````` (* 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 `````` Andrei Paskevich committed Jun 29, 2011 15 `````` explicit (module State) \/ global (module Random). Functions init allow `````` Jean-Christophe Filliâtre committed Jun 21, 2011 16 17 18 19 20 21 22 23 24 25 26 27 `````` to reset the generators according to a given seed. *) (* Purely applicative generators. *) theory Generator use import bool.Bool use import int.Int type generator `````` Andrei Paskevich committed Jun 29, 2011 28 `````` function create int : generator `````` Jean-Christophe Filliâtre committed Jun 21, 2011 29 `````` `````` Andrei Paskevich committed Jun 29, 2011 30 `````` function next generator : generator `````` Jean-Christophe Filliâtre committed Jun 21, 2011 31 `````` `````` Andrei Paskevich committed Jun 29, 2011 32 `````` function get_bool generator : bool `````` Jean-Christophe Filliâtre committed Jun 21, 2011 33 `````` `````` Andrei Paskevich committed Jun 29, 2011 34 `````` function get_int generator int : int `````` Jean-Christophe Filliâtre committed Jun 21, 2011 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 `````` 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 `````` Andrei Paskevich committed Jun 29, 2011 64 `````` { s.state = next (old s.state) /\ result = get_bool s.state } `````` Jean-Christophe Filliâtre committed Jun 21, 2011 65 66 67 68 `````` parameter random_int (s: state) (n: int) : { 0 < n } int writes s `````` Andrei Paskevich committed Jun 29, 2011 69 `````` { s.state = next (old s.state) /\ result = get_int s.state n /\ `````` Jean-Christophe Filliâtre committed Jun 21, 2011 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 `````` 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 `````` Andrei Paskevich committed Jun 29, 2011 92 `````` { s.state = next (old s.state) /\ result = get_bool s.state } `````` Jean-Christophe Filliâtre committed Jun 21, 2011 93 94 95 96 `````` let random_int (n: int) = { 0 < n } random_int s n `````` Andrei Paskevich committed Jun 29, 2011 97 `````` { s.state = next (old s.state) /\ result = get_int s.state n /\ `````` Jean-Christophe Filliâtre committed Jun 21, 2011 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 `````` 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: *)``````