vacid_0_build_maze.mlw 4.52 KB
Newer Older
1

2
theory UnionFind_pure
3

4 5
  use import int.Int

6
  type uf_pure
7

8 9 10
  predicate repr uf_pure int int
  function size uf_pure : int
  function num uf_pure : int
11

12
  axiom Repr_function_1:
13
    forall u:uf_pure, 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

16
  axiom Repr_function_2:
17
    forall u:uf_pure, x y z:int.
18 19
    0 <= x < size u -> repr u x y -> repr u x z -> y = z

20 21
  predicate same (u:uf_pure) (x y:int) =
    forall r:int. repr u x r <-> repr u y r
22

23
  predicate same_reprs (u1 u2 : uf_pure) =
24
     forall x r:int. repr u1 x r <-> repr u2 x r
25 26

  axiom OneClass :
27
    forall u:uf_pure. num u = 1 ->
28
    forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
29

30 31 32 33 34
end

module UnionFind_sig

  use import int.Int
35
  use export UnionFind_pure
36

37
  type uf model { mutable state : uf_pure }
38

39
  val create (n:int) : uf
40
    requires { 0 <= n }
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
    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 }

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

65 66 67 68 69
end

theory Graph

  type vertex
70 71 72

  type graph

73
  inductive path graph vertex vertex =
74 75
    | 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
76 77
    | Path_trans:
        forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
78

79
end
80

81 82 83
module Graph_sig

  use import int.Int
84
  use import ref.Ref
85

86
  clone export Graph with type vertex = int
87

88
  val graph : ref graph
89

90
  val num_edges : ref int
91

92 93 94
  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 /\
95
      (forall x y:int.
96 97 98 99
        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) }
100

101 102 103 104 105
end

module BuildMaze

  use import int.Int
106
  use import ref.Ref
107

108 109
  use import UnionFind_sig
  use import Graph_sig
110

111
  val rand (s:int) : int requires { 0 < s } ensures { 0 <= result < s }
112 113 114 115

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

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

161
end