vacid_0_build_maze.mlw 4.82 KB
Newer Older
1

2 3 4 5 6 7
(* Building a perfect maze using the union-find data structure
   (from the VACID-0 Benchmarks http://vacid.codeplex.com/)

   Jean-Christophe Filliâtre (CNRS)
   Andrei Paskevich (Univ Paris Sud) *)

8
theory UnionFind_pure
9

10
  use int.Int
11

12
  type uf_pure
13

14 15 16
  predicate repr uf_pure int int
  function size uf_pure : int
  function num uf_pure : int
17

18
  axiom Repr_function_1:
19
    forall u:uf_pure, x:int.
20
    0 <= x < size u -> exists y:int. 0 <= y < size u /\ repr u x y
21

22
  axiom Repr_function_2:
23
    forall u:uf_pure, x y z:int.
24 25
    0 <= x < size u -> repr u x y -> repr u x z -> y = z

26 27
  predicate same (u:uf_pure) (x y:int) =
    forall r:int. repr u x r <-> repr u y r
28

29
  predicate same_reprs (u1 u2 : uf_pure) =
30
     forall x r:int. repr u1 x r <-> repr u2 x r
31 32

  axiom OneClass :
33
    forall u:uf_pure. num u = 1 ->
34
    forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
35

36 37 38 39
end

module UnionFind_sig

40
  use int.Int
41
  use export UnionFind_pure
42

43
  type uf = private { ghost mutable state : uf_pure }
44

45
  val create (n:int) : uf
46
    requires { 0 <= n }
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
    ensures { num result.state = n /\ size result.state = n /\
      forall x:int. 0 <= x < n -> repr result.state x x }

  val find (u:uf) (x:int) : int writes {u}
    requires { 0 <= x < size u.state }
    ensures { repr u.state x result /\
      size u.state = size (old u.state) /\
      num u.state = num (old u.state) /\
      same_reprs u.state (old u.state) }

  val union (u:uf) (a:int) (b:int) : unit writes {u}
    requires { 0 <= a < size u.state /\
               0 <= b < size u.state /\ not same u.state a b }
    ensures { same u.state a b /\
      size u.state = size (old u.state) /\
      num u.state = num (old u.state) - 1 /\
      forall x y:int. 0 <= x < size u.state -> 0 <= y < size u.state ->
        same u.state x y <->
        same (old u.state) x y \/
        same (old u.state) x a /\ same (old u.state) b y \/
        same (old u.state) x b /\ same (old u.state) a y }

69
  val get_num_classes (u:uf) : int ensures { result = num u.state }
70

71 72 73 74 75
end

theory Graph

  type vertex
76 77 78

  type graph

79
  inductive path graph vertex vertex =
80 81
    | 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
82 83
    | Path_trans:
        forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
84

85
end
86

87 88
module Graph_sig

89 90
  use int.Int
  use ref.Ref
91

92
  clone export Graph with type vertex = int
93

94
  val graph : ref graph
95

96
  val num_edges : ref int
97

98 99 100
  val add_edge (a:int) (b:int) : unit writes {num_edges,graph}
    requires { not path !graph a b }
    ensures { !num_edges = old !num_edges + 1 /\
101
      (forall x y:int.
102 103 104 105
        path !graph x y <->
        path (old !graph) x y \/
        path (old !graph) x a /\ path (old !graph) b y \/
        path (old !graph) x b /\ path (old !graph) a y) }
106

107 108 109 110
end

module BuildMaze

111 112
  use int.Int
  use ref.Ref
113

114 115
  use UnionFind_sig
  use Graph_sig
116

117
  val rand (s:int) : int requires { 0 < s } ensures { 0 <= result < s }
118 119 120 121

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

122 123 124
  let add_edge_and_union (u: uf) (a:int) (b:int)
    requires { 0 <= a < size u.state /\ 0 <= b < size u.state /\
      not same u.state a b /\ not path !graph a b /\
125
      forall x y:int.
126 127
        0 <= x < size u.state -> 0 <= y < size u.state ->
        same u.state x y <-> path !graph x y }
128
    ensures { !num_edges = old !num_edges + 1 /\
129 130 131
      same u.state a b /\
      size u.state = size (old u.state) /\
      num u.state = num (old u.state) - 1 /\
132
      (forall x y:int.
133 134
         0 <= x < size u.state -> 0 <= y < size u.state ->
         same u.state x y <-> path !graph x y) }
135 136 137 138 139 140
  = add_edge a b;
    union u a b

let build_maze (n:int)
  requires { 1 <= n /\ !num_edges = 0 /\
    forall x y:int. x=y <-> path !graph x y }
141 142 143
  diverges (* termination is only almost sure,
              assuming rand is well distributed.
              See http://toccata.lri.fr/gallery/RandomWalk.en.html *)
144 145 146
  ensures { !num_edges = n*n-1 /\
    forall x y:int. 0 <= x < n*n -> 0 <= y < n*n -> path !graph x y }
  = let u = create (n*n) in
147
    assert { forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
148
      same u.state x y -> (repr u.state x y && repr u.state x x && x = y) };
149
    while get_num_classes u > 1 do
150
      invariant {
151 152 153 154
        1 <= num u.state /\
        num u.state + !num_edges = size u.state = n*n /\
        forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
                        (same u.state x y <-> path !graph x y) }
155 156
      let x = rand n in
      let y = rand n in
157 158 159 160
      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
161 162 163 164 165 166 167 168 169
        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

170
end