Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

union_find.mlw 6.23 KB
Newer Older
1 2
module Intf

3
  use int.Int
4

5 6 7
  type t = private {
                  size: int;        (* elements are 0,1,...,size-1 *)
    ghost mutable repr: int -> int;
8 9
  } invariant {
    0 <= size /\
10 11
    (forall i. 0 <= i < size -> 0 <= repr i < size) /\
    (forall i. 0 <= i < size -> repr (repr i) = repr i)
12 13 14 15 16 17 18
  } by { size = 0; repr = fun i -> i }

  val create (n: int) : t
    requires { 0 <= n }
    ensures  { result.size = n }
    ensures  { forall i. 0 <= i < result.size -> result.repr i = i }

19 20 21 22 23 24 25 26 27 28
  val find (uf: t) (x: int) : int
    requires { 0 <= x < uf.size }
    ensures  { result = uf.repr x }

  predicate same (repr: int -> int) (x y: int) =
    repr x = repr y

  val union (uf: t) (x y: int) : unit
    requires { 0 <= x < uf.size }
    requires { 0 <= y < uf.size }
29
    writes   { uf.repr }
30 31 32 33 34 35
    ensures  { same uf.repr x y }
    ensures  { forall i j. 0 <= i < uf.size -> 0 <= j < uf.size ->
               same uf.repr i j <->
                 same (old uf.repr) i j \/
                 same (old uf.repr) i x /\ same (old uf.repr) y j \/
                 same (old uf.repr) i y /\ same (old uf.repr) x j }
36 37 38 39 40

end

module Impl

41 42
  use int.Int
  use array.Array
43

44
  (* there is a path from x to y of length at most d *)
45
  inductive path (size: int) (link: array int) (x d y: int) =
46 47 48
  | path_zero: forall size link x d.
               0 <= x < size -> link[x] = x -> 0 <= d ->
               path size link x d x
49 50
  | path_succ: forall size link.
               forall x d z. 0 <= x < size -> link[x] <> x ->
51 52
               path size link link[x] d z ->
               path size link x (d + 1) z
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67

  lemma path_dist_nonneg:
    forall size link x d y. path size link x d y -> 0 <= d

  lemma path_src:
    forall size link x d y. path size link x d y -> 0 <= x < size

  lemma path_dst:
    forall size link x d y. path size link x d y -> 0 <= y < size

  let rec lemma path_unique (size: int) (link: array int) (x d1 d2 y1 y2: int)
    requires { length link = size }
    requires { path size link x d1 y1 }
    requires { path size link x d2 y2 }
    variant  { d1 + d2 }
68
    ensures  { y1 = y2 }
69 70 71 72 73 74 75 76
  = if x <> link[x] then begin
      path_unique size link link[x] (d1-1) (d2-1) y1 y2;
    end

  let rec lemma path_last (size: int) (link: array int) (x d y: int)
    requires { length link = size }
    requires { path size link x d y }
    variant  { d }
77 78
    ensures  { link[y] = y }
  = if x <> link[x] then path_last size link link[x] (d-1) y
79 80 81 82

  type t = {
                  size: int;        (* elements are 0,1,...,size-1 *)
                  link: array int;
83
                  rank: array int;
84 85 86
    ghost mutable repr: int -> int;
    ghost mutable dist: int -> int;
  } invariant {
87
    0 <= size = length link = length rank /\
88
    (forall i. 0 <= i < size -> 0 <= repr i < size) /\
89 90
    (forall i. 0 <= i < size -> repr (repr i) = repr i) /\
    (forall i. 0 <= i < size -> link[i] <> i -> dist link[i] < dist i) /\
91 92
    (forall i. 0 <= i < size -> path size link i (dist i) (repr i))
  } by {
93
    size = 0; link = Array.make 0 0; rank = Array.make 0 0;
94
    repr = (fun i -> i); dist = (fun _i -> 0)
95 96 97 98 99 100
  }

  let create (n: int) : t
    requires { 0 <= n }
    ensures  { result.size = n }
    ensures  { forall i. 0 <= i < result.size -> result.repr i = i }
101
  = let link = Array.make n 0 in
102
    for i = 0 to n - 1 do
103 104
      invariant { forall j. 0 <= j < i -> link[j] = j }
      link[i] <- i
105
    done;
106 107
    let rank = Array.make n 0 in
    { size = n; link = link; rank = rank;
108
      repr = (fun i -> i); dist = (fun _i -> 0) }
109

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
  let rec lemma path_dist (size: int) (link: array int) (dist: int -> int)
                          (x d y: int)
    requires { length link = size }
    requires { path size link x d y }
    requires { forall i. 0 <= i < size -> link[i] <> i -> dist link[i] < dist i}
    requires { x <> y }
    variant  { d }
    ensures  { dist y < dist x }
  = if x <> link[x] && link[x] <> y then
      path_dist size link dist link[x] (d-1) y

  let rec lemma path_compression
    (size: int) (link: array int) (x dx rx: int) (i di ri: int)
    requires { length link = size }
    requires { path size link x dx rx }
    requires { x <> rx }
    requires { path size link i di ri }
    variant  { di }
    ensures  { path size link[x <- rx] i di ri }
  = if i = x then ()
    else if link[i] = i then ()
    else path_compression size link x dx rx link[i] (di-1) ri

133 134
  let rec find (uf: t) (x: int) : int
    requires { 0 <= x < uf.size }
135
    writes   { uf.link(* , uf.dist *) }
136 137 138 139 140 141 142
    variant  { uf.dist x }
    ensures  { result = uf.repr x }
    ensures  { path uf.size uf.link x (uf.dist x) result }
  = let y = uf.link[x] in
    if y <> x then begin
      assert { path uf.size uf.link y (uf.dist x - 1) (uf.repr x) };
      let r = find uf y in
143
      assert { x <> r };
144
      uf.link[x] <- r; (* path compression *)
145 146 147 148 149 150 151
      r
    end else
      x

  predicate same (repr: int -> int) (x y: int) =
    repr x = repr y

152 153 154
  let union (uf: t) (x y: int) : unit
    requires { 0 <= x < uf.size }
    requires { 0 <= y < uf.size }
155
    writes   { uf.link, uf.rank, uf.repr, uf.dist }
156 157 158 159 160 161 162 163 164
    ensures  { same uf.repr x y }
    ensures  { forall i j. 0 <= i < uf.size -> 0 <= j < uf.size ->
               same uf.repr i j <->
                 same (old uf.repr) i j \/
                 same (old uf.repr) i x /\ same (old uf.repr) y j \/
                 same (old uf.repr) i y /\ same (old uf.repr) x j }
  = let rx = find uf x in
    let ry = find uf y in
    if rx <> ry then
165 166
      let oldr = uf.repr in
      let oldd = uf.dist in
167 168 169
      if uf.rank[rx] <= uf.rank[ry] then begin
        uf.link[rx] <- ry;
        uf.repr <- (fun i -> if oldr i = rx then ry else oldr i);
170
        uf.dist <- pure { fun i -> if oldr i = rx then oldd i + 1 else oldd i };
171 172 173 174 175 176 177 178 179 180 181 182 183
        assert { forall i. 0 <= i < uf.size ->
             if oldr i = rx then path uf.size uf.link i (oldd i + 1) ry
                            else path uf.size uf.link i (oldd i)     (oldr i)};
        if uf.rank[rx] = uf.rank[ry] then
          uf.rank[ry] <- uf.rank[ry] + 1
      end else begin
        uf.link[ry] <- rx;
        uf.repr <- (fun i -> if oldr i = ry then rx else oldr i);
        uf.dist <-
          pure { fun i -> if oldr i = ry then oldd i + 1 else oldd i };

      end

184
  clone Intf with
185 186 187 188
    type t = t,
    val  create = create,
    val  find = find,
    val  union = union
189 190

end