Inverse command correctness (source code)

= Inverse command correctness

An undoable command records enough information to restore its input state when applied immediately after its corresponding edit. In a <sequence>, insertion at index $i$ is reversed by deletion at $i$; deletion is reversed by reinsertion of the saved value. If a move places an entry at final index $j$ after removing it from index $i$, the inverse moves it from $j$ back to $i$. Removing the moved entry recovers the original <sequence> with exactly that entry missing, which proves the inverse for both directions and for $i=j$.

These local inverse identities extend to a history by applying inverses in reverse chronological order. A <stack> of completed commands and a <stack> of undone commands maintain that order. A fresh command invalidates the old redo branch. Arbitrary inverses after unrelated intervening edits need not satisfy the restoration identity. State snapshots in the <Memento pattern> supply a different way to realize the same chronological undo/redo contract.