vacid_0_build_maze.mlw 4.3 KB
Newer Older
1 2

theory UnionFind
3

4 5
  use import int.Int

6 7
  type uf

Andrei Paskevich's avatar
Andrei Paskevich committed
8 9 10
  predicate repr uf int int
  function size uf : int
  function num uf : int
11

12
  axiom Repr_function_1:
13
    forall u:uf, x:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
14
    0 <= x < size u -> exists y:int. 0 <= y < size u /\ repr u x y
15
  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

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  predicate same (u:uf) (x y:int) =
20
     forall r:int. repr u x r <-> repr u y r
21

Andrei Paskevich's avatar
Andrei Paskevich committed
22
  predicate same_reprs (u1 u2 : uf) =
23
     forall x r:int. repr u1 x r <-> repr u2 x r
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
28

29 30 31 32 33
end

module UnionFind_sig

  use import int.Int
34
  use import ref.Ref
35 36 37

  use export UnionFind

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  val create (n:int) : ref uf
    requires { 0 <= n }
    ensures { num !result = n /\ size !result = n /\
      forall x:int. 0 <= x < n -> repr !result x x }

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

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

  val get_num_classes (u:ref uf) : int reads {u} ensures { result = num !u }
60

61 62 63 64 65
end

theory Graph

  type vertex
66 67 68

  type graph

69
  inductive path graph vertex vertex =
70 71
    | 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
72 73
    | Path_trans:
        forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
74

75
end
76

77
theory Graph_int
78

79
  clone export Graph with type vertex = int
80

81 82 83 84 85
end

module Graph_sig

  use import int.Int
86
  use import ref.Ref
87

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

91
  val graph : ref graph
92

93
  val num_edges : ref int
94

95 96 97
  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 /\
98
      (forall x y:int.
99
          path !graph x y <->
Andrei Paskevich's avatar
Andrei Paskevich committed
100 101
          path (old !graph) x y \/
          path (old !graph) x a /\ path (old !graph) b y \/
102
          path (old !graph) x b /\ path (old !graph) a y) }
103

104 105 106 107 108
end

module BuildMaze

  use import int.Int
109
  use import ref.Ref
110

111 112
  use import UnionFind_sig
  use import Graph_sig
113

114
  val rand (s:int) : int requires { 0 < s } ensures { 0 <= result < s }
115 116 117 118

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

119 120
  let add_edge_and_union (u: ref uf) (a:int) (b:int)
    requires { 0 <= a < size !u /\ 0 <= b < size !u /\
Andrei Paskevich's avatar
Andrei Paskevich committed
121
      not same !u a b /\ not path !graph a b /\
122
      forall x y:int.
123
        0 <= x < size !u -> 0 <= y < size !u ->
124 125
        same !u x y <-> path !graph x y }
    ensures { !num_edges = old !num_edges + 1 /\
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127
      same !u a b /\
      size !u = size (old !u) /\ num !u = num (old !u) - 1 /\
128
      (forall x y:int.
129
         0 <= x < size !u -> 0 <= y < size !u ->
130 131 132 133 134 135 136 137 138 139
         same !u x y <-> path !graph x y) }
  = 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 }
  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
140
    assert { forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
141
             same !u x y -> (repr !u x y && repr !u x x && x = y) };
142
    while get_num_classes u > 1 do
143 144
      invariant {
          1 <= num !u /\ num !u + !num_edges = size !u = n*n /\
145
          forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
146
                          (same !u x y <-> path !graph x y) }
147 148
      let x = rand n in
      let y = rand n in
149 150 151 152
      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
153 154 155 156 157 158 159 160 161
        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

162
end