vacid_0_build_maze.mlw 4.39 KB
Newer Older
1 2

theory UnionFind
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
3

4 5
  use import int.Int

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6 7
  type uf

8
  logic repr uf int int
9 10
  logic size uf : int
  logic num uf : int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

12
  axiom Repr_function_1:
13
    forall u:uf, x:int.
14 15
    0 <= x < size u -> exists y:int. 0 <= y < size u and repr u x y
  axiom Repr_function_2:
16
    forall u:uf, x y z:int.
17 18
    0 <= x < size u -> repr u x y -> repr u x z -> y = z

19
  logic same (u:uf) (x y:int) =
20
     forall r:int. repr u x r <-> repr u y r
21

22
  logic same_reprs (u1 u2 : uf) =
23
     forall x r:int. repr u1 x r <-> repr u2 x r
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24 25

  axiom OneClass :
26
    forall u:uf. num u = 1 ->
27
    forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28

29 30 31 32 33 34 35 36 37 38 39 40 41
end

module UnionFind_sig

  use import int.Int
  use import module stdlib.Ref

  use export UnionFind

parameter create :
  n:int ->
    { 0 <= n }
    ref uf
42 43
    { num result = n and size result = n and
      forall x:int. 0 <= x < n -> repr result x x }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44

45 46 47 48 49 50 51
parameter find :
  u:ref uf -> x:int ->
    { 0 <= x < size u }
    int writes u
    { repr u x result and
      size u = size (old u) and num u = num (old u) and
      same_reprs u (old u) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52

53 54
parameter union :
  u:ref uf -> a:int -> b:int ->
55
    { 0 <= a < size u and 0 <= b < size u and not same u a b }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56
    unit writes u
57
    { same u a b and
58 59
      size u = size (old u) and num u = num (old u) - 1 and
      forall x y:int. 0 <= x < size u -> 0 <= y < size u ->
60 61 62 63
         same u x y <->
         same (old u) x y or
         same (old u) x a and same (old u) b y or
         same (old u) x b and same (old u) a y }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64

65
parameter get_num_classes :
66
  u:ref uf -> {} int reads u { result = num u }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
67 68


69 70 71 72 73
end

theory Graph

  type vertex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74 75 76

  type graph

77 78 79 80 81
  inductive path graph vertex vertex =
    | Path_refl : forall g:graph, x:vertex. path g x x
    | Path_sym  : forall g:graph, x y:vertex. path g x y -> path g y x
    | Path_trans:
        forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82

83
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

85
theory Graph_int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86

87
  clone export Graph with type vertex = int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
end

module Graph_sig

  use import int.Int
  use import module stdlib.Ref

  clone export Graph with type vertex = int
(*  use export Graph *)
(*  use export Graph_int*)

  parameter graph : ref graph

  parameter num_edges : ref int

  parameter add_edge : a:int -> b:int ->
    { not path graph a b }
    unit writes num_edges graph
107
    { num_edges = old num_edges + 1 and
108
      (forall x y:int.
109
          path graph x y <->
110
          path (old graph) x y or
111
          path (old graph) x a and path (old graph) b y or
112
          path (old graph) x b and path (old graph) a y)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113 114
   }

115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
end

module BuildMaze

  use import int.Int
  use import module stdlib.Ref

  use import module UnionFind_sig
  use import module Graph_sig

  parameter rand : s:int -> { 0 < s } int { 0 <= result < s }

  lemma Ineq1 :
    forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n

  let add_edge_and_union u (a:int) (b:int) =
    { 0 <= a < size u and 0 <= b < size u and
      not same u a b and not path graph a b and
      forall x y:int.
        0 <= x < size u -> 0 <= y < size u ->
        same u x y <-> path graph x y
    }
    add_edge a b;
    union u a b
    { num_edges = old num_edges + 1 and
      same u a b and
      size u = size (old u) and num u = num (old u) - 1 and
      (forall x y:int.
         0 <= x < size u -> 0 <= y < size u ->
         same u x y <-> path graph x y)
    }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
146 147

let build_maze (n:int) =
148 149 150
  { 1 <= n and
    num_edges = 0 and
    forall x y:int. x=y <-> path graph x y
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
151 152
  }
    let u = create (n*n) in
153
    assert { forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
154
             same u x y -> (repr u x y && repr u x x && x = y) };
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155
    while get_num_classes u > 1 do
156
      invariant
157
        { 1 <= num u and num u + num_edges = size u = n*n and
158
          forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
159
                          (same u x y <-> path graph x y)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160 161 162
        }
      let x = rand n in
      let y = rand n in
163 164 165 166
      let d = rand 2 in
      let w = if d = 0 then x+1 else x in
      let z = if d = 0 then y else y+1 in
      if w < n && z < n then begin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
167 168 169 170 171 172 173 174
        let a = y * n + x in
        assert { 0 <= a < n*n };
        let b = w * n + z in
        assert { 0 <= b < n*n };
        if find u a <> find u b then
          add_edge_and_union u a b
      end
    done
175
  { num_edges = n*n-1 and
176
    forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
177
      path graph x y }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178

179 180
end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
(*
182
Local Variables:
183
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_build_maze"
184
End:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185
*)