DFS - Proof of Correctness

Problem Detail: 

I'm currently studying the book "Introduction to Algorithms - Cormen". Although a proof of correctness for the BFS algorithm is given, there isn't one any for the DFS in the book. So I was courious about how it can be shown that DFS visits all the nodes. I also googled for it. But it seems that every lecturer do some copy-paste work from this book in their pdf's, so I couldn't find anything useful.

By DFS we had to show that it found the shortest path. But since DFS does not calculate something like that I have no idea how to prove it.

---

Off the topic, why are those proofs so important? Throughout the book there are so many lemmas and theorems which can be really boring sometimes. I understand how an algorithm works in 10 minutes, perhaps need another 5 to 10 minutes to understand how to analyse the running time, but then I'm loosing 1 hour just for some useless lemmas. Besides, and worse even, I studied almost 50 proofs/lemmas of different algorithms till now, I never managed to solve one of them by myself. How can I gain the "proving ability"? Is there a systematical way to learn that? I don't mean the Hoare logic way with invariants, rather the informal way described in the book "Introduction to Algorithms". Is there any book which focuses on "how to prove algorithms" and show that in a systematical, introductory way ?

Asked By : Schwammkopf

Answered By : ajmartin

From lecture notes by Prof. Danny Sleator:

Basic DFS algorithm: Each vertex has a binary field called "visited(v)". Here's the algorithm in pseudo-code:

 for all v in V do visited(v) = 0  for all v in V do if (visited(v)==0) DFS(v)      DFS(v) {       visited(v) = 1       for all w in adj(v) do if (visited(w)==0) DFS(w)    } 

Claim 1: DFS is called exactly once for each vertex in the graph.

Proof: Clearly DFS(x) is called for a vertex x only if visited(x)==0. The moment it's called, visited(x) is set to 1. Therefore the DFS(x) cannot be called more than once for any vertex x. Furthermore, the loop "for all v...DFS(v)" ensures that it will be called for every vertex at least once. QED.

Claim 2: The body of the "for all w" loop is executed exactly once for each edge (v,w) in the graph.

Proof: DFS(v) is called exactly once for each vertex v (Claim 1). And the body of the loop is executed once for all the edges out of v. QED.

Therefore the running time of the DFS algorithm is O(n+m).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/7749