Proving breath first traversal on graphs

Question

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

Reach := {u}
LastCardinality := 0
while LastCardinality < |Reach| do
  LastCardinality := |Reach|
  Next := null
  foreach i <- Reach do
    foreach j <- V do
      if(i,j) exists in E then
        Next := Next + {j}
  Reach := Reach + Next
return Reach

So far I have got that the output needs to be Reach = Goal where Goal = {r | r exists V, there is a path from u to r}. I also have three invariants that I am pretty sure will help prove this.

Reach is always a subset of Goal and Next is always a subset of Goal.

After an arbitrary K times through the while loop, for every t that exsits in V, if t has a path of length k+1 from u, then t exists in Reach

If Reach is a subset of Goal before the while loop then LastCardinality < |Reach|

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 proof those three characteristics about an algorithm?

Answer 1

Hint 1 You want to claim that at the end of $k$ iterations, all vertices $v$ which have a $u \to v$ path in $G$ of length at most $k$ are in $\textrm{Reach}$.

Proceed by induction on $k$, the base case is trivial (take $k=0$ if you are lazy and $k=1$ if you are not).

Now in the inductive step, assume upto $k$ and prove for $k+1$. So let $v \in V$ be such a vertex, which has a path in $G$ of length $k+1$. Then, the previous vertex on that path, say $x$, is at most $k$ edges away from $u$, now use the Inductive Hypothesis and you are done.

Hint 2 Now use the claim to prove that the algorithm returns all vertices in the connected component of $u$.