Correctness

Algorithm terminates because Visit only performs work on white nodes and instantly makes the visted node non-white. Thus, impossible to recurse forever.

Correctness proof by induction on the length of the constructed list.

• Inductive hypothesis: When a node is added to the list, all its children are already in the list. Therefore, all edges in the DAG point to the right.
• The first node added to the list will be one with no outgoing edges.
• Any node added to the list has no white kids. In fact, it has no gray kids, either (why?).

• Therefore, all its kids are black and have already been added to the list.
• Therefore, it's ok to add it to the front of the list.