Consider the following graph search loop:
do whatever you need to do with v record that v has been visited put the edges leaving v into the dispenser while the dispenser is not empty retrieve and remove edge e from the dispenser let w be the head of e if w has not been visited do whatever you need to do with e do whatever you need to do with w record that w has been visited put the edges leaving w into the dispenser endif endwhile
This loop has the following invariants:
As a consequence of the above invariants, we get a third invariant:
This means that the edges connect the visited vertices and they do not form any cycles.
For some optimization conditions, MST and SSSP, for example, we can use a priority queue for the dispenser and set up the prioritization so that the third invariant can be strengthened to the following: