DFS - Proof of Correctness

Question

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 ?

Answer 1

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).

Answer 2

I had the same problem when I was an undergrad. I can see you understand the algorithm. And, to prove that it works is to explain it formally that it works.

Why we have many proofs ? because we may have algorithms that are not correct, and we need to show that our algorithm is correct and actually work always!.

Same for the analysis. If we want to prove for example that our algorithm is better than others, then we prove it. You may tell me that we can implement our algorithm and and test it, but this does not consider all the possible cases of input. Therefore, what we do is to prove it.

(We usually prove the correctness and complexity of an algorithm (which is a measure of its performance)).

This is just an answer for your second question. For your first question, a hint is to say why we will visit every other vertex if the graph is connected. [Hint: because the graph is connected than for every pair of vertices there is a path.] ...(back to your second question).. if you note here that I am using one fact to prove my original fact (i.e., there is a path connecting every pair of nodes --> DFS is correct). The first fact is clear in our case given the definition of connectivity. In many other cases, it is not clear. So we will need to prove one fact by proving another, and perhaps do that again and again. This is why we have a lot of lemmas and theorems.

They are boring now. but once you see their magic, you will love them ! As a fun excercise try to solve simple algorithmic problems and prove their correctness and analyses. To verify your answers, re-read your answers. If they convince you, then you are correct. If not, then re-do it again.

Answer 3

AJed puts things very nicely, and ajmartin has provided you with a proof too. I would like to add the following to your second question:

If you really understood the algorithm, then you should also understand these properties of the algorithm, and be able to explain them to others informally - say to friends or colleagues (such as how and why a shortest path is found). If you don't realize these properties on your own, you should at least realize them once you are told (such as by being asked to prove them). If you can do that, from there it is just a matter of writing down things formally (which can be achieved with practice). If you can't explain that, or don't understand things like why it visits every node, then you have not really understood the algorithm - just understood how to implement it.

I know proofs are often written in a more complicated manner than necessary. And can be difficult to understand easily. But that should not undermine the importance of proofs - it just shows proofs should be as simple as possible without being ambiguous/loose/incorrect.

Proofs make things water-tight. It allows the algorithm to form the basis of more complex analysis/algorithms/theories without having to be re-assessed. You need to show that the algorithm is correct for all inputs that it claims to handle. Just intuition may not always be sufficient (or sometimes may also be misleading). You say that in software development, there are ways to test things for most cases. But if the algorithm is proven correct, all you need to check is that the algorithm has been implemented correctly.

Put another way, what if someday you come up with a brilliant algorithm for some problem in your work. The algorithm is complex and no-one understands it. How do you convince others that the algorithm works, and that they could use it too? Equally (or more?) importantly, how would you convince your boss that your brilliant idea actually works and won't cause cataclysmic failures for some cases which have not been tested - especially since no one else has used the algorithm before? The answer is you prove the correctness of your algorithm, and show that it has been correctly implemented. You need proof techniques for that, and so are taught these in university - unlike your claim in your comment as posted as answer - it is not something only useful for masters or phd.

A side-effect of proofs is that they often offer deeper insight into the algorithm. Taking the very trivial case of your question, if you read a proof of why every edge and vertex is visited exactly once, or why and how it finds a shortest path, you will be able to better understand and visualize the working of the algorithm.

As for why there are so many lemmas, it is the same thing as programming. You could write the whole block of proof at once (as you could write the whole code in one chunk), but that would be unwieldy, tough to understand and error-prone. If, however, you write modular code, it becomes easy to re-use the modules (functions/classes), easier to test, verify, understand and abstract out complications. The same is true for proofs. You break it down into simpler "modules" - they are just called lemmas/claims etc. You get more or less the same benefits from lemmas that you get from modular code.