Search code examples
algorithmgraph-algorithmdiscrete-mathematicsproof

Proving breadth-first traversal on graphs

I am trying to prove the following algorithm to see if a there exists a path from u to v in a graph G = (V,E).

I know that to finish up the proof, I need to prove termination, the invariants, and correctness but I have no idea how. I think I need to use induction on the while loop but I am not exactly sure how.

How do I prove those three characteristics about an algorithm?

Solution

  • Disclaimer: I don't know how much formal you want your proof to be and I'm not familiar with formal proofs.

    1. induction on the while loop: Is it true at the beginning? Does it remain true after a step (quite simple path property)?
    2. same idea, induction on k (why k+1???): Is it true at the beginning? Does it remain true after a step (quite simple path property)?
    3. Think Reach as a strictly increasing set.

    Termination: maybe you can use a quite simple property linked to the diameter of the graph?

    (This question could probably be better answered elsewhere, on https://cstheory.stackexchange.com/ maybe?)