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.