Pointer Reversal (Invariante)

ursprünglicher Graph G₀ mathend000#, aktueller Graph G mathend000#:

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 mathend000# (parent), c mathend000# (current).

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

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