Given the following algorithm for a breadth first search of a graph, using queues.

Code:
Set the distances for each node to infinity
Enqueue the starting node, and set distance of the node to zero.
While the queue is not empty {
Dequeue the first element in the queue
Enqueue all the nodes adjacent to the node we just dequeued
Update the distances of each of the nodes we just enqueued
}
Prove that for any two elements in the queue u and v. $|dist(u) - dist(v)| \leq 1$. A hint provided to me was to prove a stronger statement about the ordering of the elements in the queue.

So, I thought if I could prove via induction that if u is closer to the front than v in queue then $dist(u) \leq dist(v)$, and that $|dist(front) - dist(back)| \leq 1$. But I am having troubles with it.

Is my idea good, or is there an easier property I could prove? If what I have is good, how could I prove it?

2. I've managed to prove that:

for $i if and only if $dist(u_i) \leq dist(u_j)$

However, I am still having troubles proving the statement on the right.
I am thinking either I have to do induction of the number of loops performed by the alogrithm, or i could do a proof by contradiction but I can't seem to get either to work.

3. Originally Posted by Haven
I've managed to prove that:

for $i if and only if $dist(u_i) \leq dist(u_j)$

However, I am still having troubles proving the statement on the right.
I am thinking either I have to do induction of the number of loops performed by the alogrithm, or i could do a proof by contradiction but I can't seem to get either to work.
Maybe this is just me being dumb, but the last line within the while loop is:

"Update the distances of each of the nodes we just enqueued."

Doesn't the algorithm need to specify how we update the distances?

Edit: Making some massive assumptions on what is meant by the problem statement, we have:

Assumption 1: dist(u) signifies the distance from node u to the starting node.

Assumption 2: The true distance between any two adjacent nodes is 1.

Assumption 3: We are setting all the distances to infinity initially so that we can distinguish between visited and non-visited nodes.

Assumption 4: We will not add a node to the queue if it has already been visited.

Then it seems we are dealing with an algorithm that assigns to each node the distance between it and the starting node, and it should be clear that since a queue is FIFO, when the front of the queue (which contains the oldest elements) has elements distance n from the starting node, the back of the queue (newest elements) has either elements distance n from the starting node, or distance n+1, because we won't get to distance n+2 (if there are any such nodes) until all the distance n nodes are dequeued (this is not a very rigorous explanation, but you should get the idea).

Edit 2: Sorry, I switched the words "front" and "back" which was silly.

4. It's my fault for oversimplification.

let S = the node that was just dequeued in the loop.
The distances of the nodes we enqueue is dist(S)+1

5. Originally Posted by Haven
It's my fault for oversimplification.

let S = the node that was just dequeued in the loop.
The distances of the nodes we enqueue is dist(S)+1
I edited my post above. I think it addresses your question. Let me know. (I didn't see your post #4 until just now.)

6. I understand your explanation, but I am having difficulties proving it.
I've tried to prove it as a loop invariant, but I can't get it to work.

assume we have performed k iterations of the loop and the property
$dist(u_i) \leq dist(u_j)$ for $i
holds for all the nodes in the queue thus far.

If we dequeue the first node and enqueue it's neighboring nodes, one of which being $u_t$
Then it is clear that $dist(u_t) = dist(u_1) + 1$
However I can't seem to show that for any i
$dist(u_i) \leq dist(u_t) = dist(u_1)+1$

7. Originally Posted by Haven
I understand your explanation, but I am having difficulties proving it.
I've tried to prove it as a loop invariant, but I can't get it to work.

assume we have performed k iterations of the loop and the property
$dist(u_i) \leq dist(u_j)$ for $i
holds for all the nodes in the queue thus far.

If we dequeue the first node and enqueue it's neighboring nodes, one of which being $u_t$
Then it is clear that $dist(u_t) = dist(u_1) + 1$
However I can't seem to show that for any i
$dist(u_i) \leq dist(u_t) = dist(u_1)+1$
Okay so intuitively it's already clear, and the only problem is with formalising.

Maybe break into cases:

Case 1: the queue is empty.

Case 2: the queue has one element.

Case 3: the queue has more than one element, and the first (oldest) element has the same distance as the last (newest) element.

Case 4: the queue has more than one element, and the first element has a distance one less than the distance of the last element.

The proof would then proceed to show that these are all the possible cases; that is, if we consider these cases to be states, then it is a closed system. (Show which states can lead to which other states.)

Edit: Actually, something more along the lines of your current proof, can't you just show that the distance between the first element and last element is at most 1, call them distances n and n+1, and then from this reason that since distance must be integer, and because of the ordering you determined, therefore all nodes must have distance in {n, n+1}.

8. Sorry for so many edits. I edited my latest post and am making this post just in case you're using email notification and would not otherwise notice..