dijkstra.mlw 5.99 KB
Newer Older
1
{
2
  use set.Fset as S
3
  use array.Array as M
4
5
6
7
8
}

(* iteration on a set *)

parameter set_has_next : 
9
  s:ref (S.t 'a) -> 
10
11
    {} 
    bool reads s 
12
    { if result=True then S.is_empty !s else not S.is_empty !s }
13

14
parameter set_next :
15
  s:ref (S.t 'a) -> 
16
    { not S.is_empty !s }
17
    'a writes s 
18
    { S.mem result (old !s) and !s = S.remove result (old !s) }
19
20
21

{
(* the graph *)
22

23
type vertex
24

25
logic v : S.t vertex
26

27
logic g_succ(vertex) : S.t vertex
28

29
axiom G_succ_sound : 
30
  forall x:vertex. S.subset (g_succ x) v
31

32
logic weight vertex vertex : int (* edge weight, if there is an edge *)
33

34
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
35
36
37
38
39
40
41
}

parameter eq_vertex : 
  x:vertex -> y:vertex -> {} bool { if result=True then x=y else x<>y }

(* visited vertices *)

42
parameter visited : ref (S.t vertex)
43
44

parameter visited_add : 
45
  x:vertex -> {} unit writes visited { !visited = S.add x (old !visited) }
46

47
48
(* current distances *)

49
parameter d : ref (M.t vertex int)
50
51
52

(* priority queue *)

53
parameter q : ref (S.t vertex)
54
55
56
57
58

parameter q_is_empty : 
  unit -> 
    {} 
    bool reads q 
59
    { if result=True then S.is_empty !q else not S.is_empty !q }
60
61
62
63
64

parameter init :
  src:vertex ->
    {} 
    unit writes visited, q, d 
65
66
    { S.is_empty !visited and 
      !q = S.add src S.empty and 
67
      !d = M.set (old !d) src 0  }
68

69
70
71
72
73
74
75
76
77
78
79
80
81
let relax u v =
  {}
  if not (S.mem v !visited) then
    let x = M.get !d u + weight u v in
    if S.mem v !q then begin
      if x < M.get !d v then d := M.set !d v x
    end else begin
      q := S.add v !q;
      d := M.set !d v x
    end
  { (S.mem v !visited and !q = old !q and !d = old !d) 
    or
    (S.mem v !q and M.get !d u + weight u v >= M.get !d v and 
82
        !q = old !q and !d = old !d) 
83
84
85
86
    or	
    (S.mem v !q  and M.get (old !d) u + weight u v < M.get (old !d) v and 
        !q = old !q and !d = M.set (old !d) v (M.get (old !d) u + weight u v))
    or
87
    (not S.mem v !visited and not S.mem v (old !q) and !q = S.add v (old !q) and
88
        !d = M.set (old !d) v (M.get (old !d) u + weight u v)) }	
89
90

{
91
logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
92
  S.mem m q and 
93
  forall x:vertex. S.mem x q -> M.get d m <= M.get d x
94
95
96
97
}

parameter q_extract_min :
  unit ->
98
    { not S.is_empty !q } 
99
    vertex reads d writes q 
100
    { min result (old !q) !d and !q = S.remove result (old !q) }
101
102

(* paths and shortest paths 
103
   path x y d = 
104
	there is a path from x to y of length d
105
   shortest_path x y d = 
106
107
108
	there is a path from x to y of length d, and no shorter path *)

{ 
109
inductive path vertex vertex int = 
110
  | Path_nil  : 
111
      forall x:vertex. path x x 0
112
  | Path_cons :   
113
      forall x y z:vertex. forall d:int. 
114
      path x y d -> S.mem z (g_succ y) -> path x z (d+weight y z)
115

116
lemma Length_nonneg : forall x y:vertex. forall d:int. path x y d -> d >= 0
117

118
logic shortest_path (x y:vertex) (d:int) =
119
  path x y d and forall d':int. path x y d' -> d <= d'
120
121

lemma Path_inversion :
122
  forall src v:vertex. forall d:int. path src v d ->
123
  (v = src and d = 0) or
124
  (exists v':vertex. path src v' (d - weight v' v) and S.mem v (g_succ v'))
125
126

lemma Path_shortest_path :
127
  forall src v:vertex. forall d:int. path src v d ->
128
  exists d':int. shortest_path src v d' and d' <= d
129
130
131
132

(* lemmas (those requiring induction) *)

lemma Main_lemma :
133
  forall src v:vertex. forall d:int. 
134
  path src v d -> not shortest_path src v d ->
135
  exists v':vertex. exists d':int. 
136
    shortest_path src v' d' and S.mem v (g_succ v') and d' + weight v' v < d
137
138

lemma Completeness_lemma :
139
  forall s:S.t vertex. forall src:vertex. forall dst:vertex. forall d:int. 
140
141
  (* if s is closed under g_succ *)
  (forall v:vertex. 
142
     S.mem v s -> forall w:vertex. S.mem w (g_succ v) -> S.mem w s) ->
143
  (* and if s contains src *)
144
  S.mem src s -> 
145
  (* then any vertex reachable from s is also in s *)
146
  path src dst d -> S.mem dst s
147
148
149

(* definitions used in loop invariants *)

150
logic inv_src (src:vertex) (s q:S.t vertex) =
151
  S.mem src s or S.mem src q
152

153
logic inv (src:vertex) (s q:S.t vertex) (d:M.t vertex int) =
154
  inv_src src s q
155
  (* S,Q are contained in V *)
156
  and S.subset s v and S.subset q v
157
158
  (* S and Q are disjoint *)
  and 
159
  (forall v:vertex. S.mem v q -> S.mem v s -> false)
160
161
  (* we already found the shortest paths for vertices in S *)
  and
162
  (forall v:vertex. S.mem v s -> shortest_path src v (M.get d v))
163
164
  (* there are paths for vertices in Q *)
  and
165
  (forall v:vertex. S.mem v q -> path src v (M.get d v))
166
167
  (* vertices at distance < min(Q) are already in S *)
  and
168
169
  (forall m:vertex. min m q d -> 
     forall x:vertex. forall dx:int. shortest_path src x dx -> 
170
       dx < M.get d m -> S.mem x s) 
171

172
logic inv_succ (src:vertex) (s q : S.t vertex) =
173
  (* successors of vertices in S are either in S or in Q *)
174
175
  (forall x:vertex. S.mem x s -> 
     forall y:vertex. S.mem y (g_succ x) -> S.mem y s or S.mem y q)
176

177
178
logic inv_succ2 (src:vertex) (s q : S.t vertex)
                (u:vertex) (su:S.t vertex) =
179
180
  (* successors of vertices in S are either in S or in Q,
     unless they are successors of u still in su *)
181
182
183
  (forall x:vertex. S.mem x s -> 
     forall y:vertex. S.mem y (g_succ x) -> 
       (x<>u or (x=u and not S.mem y su)) -> S.mem y s or S.mem y q)
184
185
186
187
188
}

(* code *)

let shortest_path_code (src:vertex) (dst:vertex) =
189
  { S.mem src v and S.mem dst v }
190
  init src;
191
  while not (q_is_empty ()) do
192
193
    invariant { inv src !visited !q !d and inv_succ src !visited !q }
    variant   { S.cardinal v - S.cardinal !visited }
194
    let u = q_extract_min () in
195
    assert { shortest_path src u (M.get !d u) };
196
197
198
199
    visited_add u;
    let su = ref (g_succ u) in
    while not (set_has_next su) do 
      invariant 
200
201
202
	{  S.subset !su (g_succ u) and
 	   inv src !visited !q !d and inv_succ2 src !visited !q u !su }
      variant { S.cardinal !su }
203
204
205
206
207
      let v = set_next su in
      relax u v
    done
  done
  { (forall v:vertex. 
208
       S.mem v !visited -> shortest_path src v (M.get !d v)) 
209
210
    and
    (forall v:vertex. 
211
       not S.mem v !visited -> forall dv:int. not path src v dv) }
212

213
214
215
216
217
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/dijkstra"
End: 
*)