How to prove that BFS directed-graph traversal algorithm terminates?

Question

How to prove that BFS directed-graph traversal algorithm terminates? (I copy the pseudocode from here) Input: A graph G and a root v of G.

  procedure BFS(G,v):
      create a queue Q
      enqueue v onto Q
      mark v
      while Q is not empty:
          t ← Q.dequeue()
          if t is what we are looking for:
              return t
          for all edges e in G.incidentEdges(t) do
             o ← G.opposite(t,e)
             if o is not marked:
                  mark o
                  enqueue o onto Q

Answer 1

The only potentially non-terminating construct used here is the while loop. So you need to prove that Q eventually becomes empty.

Q contains vertices from the graph. The only operations that add elements to Q are the enqueue operations. Each adds a single vertex. So proving the termination of the algorithm is equivalent to proving that only a finite number of enqueue operations are performed.

The first call to enqueue at the beginning of the program adds one vertex and marks it. The second call to enqueue adds a vertex that was not marked yet, and the vertex is marked at the same time.

Since a vertex is never unmarked, the set of marked vertices can only grow.

The set of marked vertices is included in the set of all vertices. Note that the graph is be assumed to be finite (in an infinite graph, the search might not terminate). Hence there are at most $|G|$ mark operations where $|G|$ is the number of vertices in the graph. Since each enqueue operation has a corresponding mark, there are at most $|G|$ enqueue operations. Therefore there are at most $|G|$ dequeue operations. Since there is one dequeue operation at each loop iteration, there are at most $|G|$ iterations of the while loop, a finite number.