@*Dijkstra's shortest path. Obviously the way to prove Dijkstra's algorithm is the way Dijsktra would do it himself. Consider @u @@; d[v] := 0; W := {v}; @@; {@tinvariant: $\forall u \in W$, $d[u]$ is the shortest distance from $v$ to $u$@> & @t$\forall u \in V-W$, $d[u] } do |W| != |V| --> @@; @@; if d[w] <= d[u] + c(u,w) --> skip [] d [w] >= d[u] + c(u,w) --> d[w] := d[u] + c(u,w) fi; W := W @t$\cup$@> {u} od @*Index.