Topological Sort
Definition A topological sort of a DAG G=(V,E) is a linear ordering of all its vertices such that if G contains an edge (u,v), then u appears before v in the ordering. (If the graph is not acyclic, then no linear ordering is possible.)
Theorem (Topological Sort Correctness) Topologoical-Sort(G) produces a topological sort of a DAG G.
Proof Suppose that DFS is run on a given DAG G=(V,E) to determin finish times for its vertices. It suffices to show that for any pair of distinct vertices u,v∈V, if there is an edge in G from u to v, then f[v]<f[u]. Consider edge (u,v) explored by DFS(G). When this edge is explored, v cannot be gray, since then v would be an ancestor of u and (u,v) would be a back edge, contradicting that this is a DAG (Theorem DAG No Back Edges). Therefore, v must be either white or black.
If v is white, it becomes a descendent of u and so f[v]<f[u].
If v is black, it has already been finished, so that f[v] has already been set. Since we are still exploring from u we have not set a timestamp for f[u] and thus f[v]<f[u].
Thus for any edge (u,v) in a DAG, we have f[v]<f[u]. (EOP)