← Dijkstra’s algorithm: Correctness by induction