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

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

random.mlw 2.47 KB
Newer Older
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's avatar
Andrei Paskevich committed
15
   explicit (module State) \/ global (module Random). Functions init allow
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's avatar
Andrei Paskevich committed
28
  function create int : generator
29

Andrei Paskevich's avatar
Andrei Paskevich committed
30
  function next generator : generator
31

Andrei Paskevich's avatar
Andrei Paskevich committed
32
  function get_bool generator : bool
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34
  function get_int  generator int : int
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's avatar
Andrei Paskevich committed
64
    { s.state = next (old s.state) /\ result = get_bool s.state }
65
66
67
68

  parameter random_int (s: state) (n: int) :
    { 0 < n }
    int writes s
Andrei Paskevich's avatar
Andrei Paskevich committed
69
    { s.state = next (old s.state) /\ result = get_int s.state n /\
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's avatar
Andrei Paskevich committed
92
    { s.state = next (old s.state) /\ result = get_bool s.state }
93
94
95
96

  let random_int (n: int) =
    { 0 < n }
    random_int s n
Andrei Paskevich's avatar
Andrei Paskevich committed
97
    { s.state = next (old s.state) /\ result = get_int s.state n /\
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:
*)