1 open list
 2 open pool
 3 
 4 (* Generic breadth-first search. *)
 5 
 6 val traverse:
 7   [unvisited, visiting, visited, p : perm]
 8   exclusive visited =>
 9   (
10     (* A pool of all nodes. *)
11     nodes: pool unvisited,
12     (* A list of the root nodes. *)
13     roots: list dynamic,
14     (* A function that changes the state of a node from [unvisited] to [visiting]. *)
15     pre: (consumes node: unvisited | p) -> (| node @ visiting),
16     (* A function that changes the state of a node from [visiting]
17        to [visited] and returns its successors. *)
18     post: (consumes node: visiting | p) -> (list dynamic | node @ visited)
19     (* The permission [p] required by [pre] and [post]. *)
20     | p
21   )
22 ->
23   (* A new pool of the visited nodes. *)
24   pool visited