I wrote the following algorithm based on BFS. The algorithm detects wether a given undirected connected 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.