# how to prove correctness of this BFS algorithm?

Given an undirected connected graph, I wrote the following algorithm based on BFS. The algorithm detects wether this graph contains a cycle. If it contains a cycle then prints it. I'm pretty sure that it works just fine, but I don't really know how to prove its correctness properly. Here is the pseudo-code:

Let s be the root
set parent[s]=s and parent[v]=null for all other v
create queue q ;
enqueue(s,q);
cycle=false;
while (!isEmpty(q) && !cycle) {
u=front(q);
for every edge (u,v) incident to u {
if (parent[v]==null){
parent[v]=u;
enqueue(v);
}
else if (parent[u]!=v){
cycle=true;
keep the edge (u,v)
}
dequeue(q);
if (cycle){
print edge (u,v)
while (parent[u]!=parent[v])&& (parent[v]!=u)&&(parent[u]!=v){
print edge (u,parent[u]) and  edge (v,parent[v])
u=parent[u];
v=parent[v];
}
if (parent[u]==parent[v])
print edge (u,parent[u]) and edge (v,parent[v])
else
print edge (u,v)
}
/**************************************************/
/**************************************************/


I've been working on the proof but i can't get through it. First i want to prove that if G contains a cycle then the algorithm does detect it. My idea is the following: Let s be the root of the bfs. We know that G contains a cycle, so there is a node such that there are two different paths from s to such a node. Let u be the first node that satisfies this. Since that BFS visits all the nodes, and explores each edge once, and also marks as visited all nodes that were visited, it will reach a step in which it is about to visit the node u for the second time and then it finds the cycle.

Then I want to prove that in the afirmative case, the edges that it prints does forms a cycle, but i'm really stuck with this.

Now assuming there is at least one cycle in the graph. Consider the set $$S$$ of vertices, that belong to a cycle and have the least possible distance to $$s$$. Any two vertices in $$S$$ can not belong to the same cycle, since then they will form a cycle with a vertex with a smaller depth in the BFS-tree, which contradicts the assumption that they are closest possible to $$s$$. All these vertices belong to the same level of the BFS-tree since they have the same distance to $$s$$. The BFS-tree branches at each of them to at least two branches. Sice they all belong to cycles in the graph, there must exist an edge between two branches from the subtree rooted at one of them. This edge has its endpoints between two nodes on the same level in the tree, since else, one of them could have been visited by the other and get a smaller depth. When visiting this edge, our algorithm detects a cycle. The Cycle is hence this edge along with both paths in the BFS-tree from a vertex $$v \in S$$, to the endpoints of this edge. We output exactly these edges, where we start by printing this edge and backtrack on both branches until we reach back the vertex $$v$$ .