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.

Commit 5251bfb1 authored by Sylvain Dailler's avatar Sylvain Dailler

Removed coq from Dijkstra.

parent 803606ff
......@@ -181,6 +181,15 @@ module DijkstraShortestPath
ensures { S.mem result (old !s) }
ensures { !s = S.remove result (old !s) }
(* Ad hoc lemma for former coq proof *)
lemma inside_or_exit:
forall s, src, v, d. S.mem src s -> path src v d ->
S.mem v s
\/
exists y. exists z. exists dy.
S.mem y s /\ not (S.mem z s) /\ S.mem z (g_succ y) /\
path src y dy /\ (dy + weight y z <= d)
(* Algorithm's code. *)
let shortest_path_code (src dst: vertex)
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment