# Correct invariant of BFS

I am trying to find a correct invariant of BFS. If we represent a queue as $$Q = [a_0;...; a_n]$$ such that : $$Q.pop() = a_n$$ then I found the following invariant which I think is correct (we denote by $$Q$$ the queue used to run the BFS, $$s$$ the node in the graph from which we begin the BFS and $$d$$ the distance between two nodes in the graph):

• all elements in $$Q$$ are in decreasing order (i.e., for all $$i , $$d(s,a_i) \geq d(s, a_j)$$ ) and $$d(s,a_n) \leq d(s,a_0) \leq d(s,a_n)+1$$.

So in the queue there aren't three nodes $$a_i, a_j, a_k$$ that are all at distinct distances from $$s$$.

So is this invariant correct? Is it the common invariant to use or we generally use a "simpler" invariant? (In this case It would be very nice if you can give this invariant.)

Thank you very much!

• @Apass.Jack Thank you, you are right I meant nodes not edges. I 've edited, hope it's better now. – Name_is_anonyme Mar 4 '19 at 15:31
• I'd suggest looking through a good algorithms textbook; it's likely to have a proof of correctness for BFS. That proof is likely to contain an invariant (either explicitly or implicitly); see what they use. That should let you figure out what is common/normal to use. I'm not sure your sufficient will be strong enough to prove the algorithm correct, but that's how to test whether your algorithm is "correct"; try proving BFS is correct using proof by induction, and see if your invariant is enough that such a proof goes through. – D.W. Mar 4 '19 at 21:35