Proving breadth-first traversal on graphs

Question

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?

Answer 1

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

Answer 2

There is a lot of possibilities. For example, for a Breadth First Search, we note that: (1) The algorithm never visits the same node twice.(as any path back must be >= the length that put it in the discovered pile already. (2) At every step, it adds exactly one node.

Thus, it clearly must terminate on any finite graph, as the set of nodes which are discoverable cannot be larger than the set of nodes which are in the graph.

Finally, since, give a start node, it will only terminate when it has reached every node which is connected by any path to the start node, it will always find a path between the start and target if it exists.

You can rewrite these logical steps above in deeper rigour if you like, for example, by showing that the list of visited nodes is strictly increasing, and non convergent (i.e. adding one to something repeatedly tends to infinity) and the termination condition must be met at at most some finite value, and a non convergent increasing function always intersects a given bound exactly once.

BFS is an easy example because it has such simple logic, but proving these things for a given algorithm may be extremely tricky.