Pointer Reversal (Invariante)

ursprünglicher Graph G₀, aktueller Graph G:

Knoten (cons) mit zwei Kindern (head, tail), markiert mit

• 0: noch nicht besucht
• 1: head wird besucht (head-Zeiger ist invertiert)
• 2: tail wird besucht (tail-Zeiger ist invertiert)
• 3: fertig

globale Variablen p (parent), c (current).

Invariante: man erhält G₀ aus G, wenn man

• head/tail-Zeiger aus 1/2-Zellen (nochmals) invertiert
• und Zeiger von p auf c hinzufügt.