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 <j$, $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!