Every information-preserving program can be run backward — and the inverse is built mechanically from the pieces of the forward program. Gries’ chapter on inversion turns “undo” into a small, provable calculus.
{P} S {Q} for a Hoare triple, guarded commands (if…fi, do…od) for the programming language, and S⁻¹ for the inverse of S. See the book for the full, rigorous treatment.Most reasoning about programs runs one way: given a start state, what does the program produce? Inversion asks the opposite question — given the result, can we recover the state we came from, and can we do it with an actual program? When the answer is yes, the inverse is not something to invent from scratch. It is assembled, construct by construct, from the forward program. This page walks the definition, the inversion rules for each command, the reasons the technique earns its place, a worked loop, and the exact conditions under which a program can be inverted at all. It builds on the basic commands and the iterative command.
A program S is invertible if there exists a program S⁻¹ — its inverse — that, run immediately after S, restores the state that held before S ran. Formally, for any predicate P describing the starting state:
Read it plainly: run S, then run S⁻¹, and you are exactly where you started. S⁻¹ undoes whatever S did. This is the same idea as ctrl-Z, but stated precisely enough to prove.
Not every program qualifies. Inversion requires that S throw away no information: the final state must uniquely determine the initial state. Two consequences follow immediately.
S could reach the same result from two different starts, no inverse could know which one to return to. A nondeterministic program is generally not invertible.x := 5, which forgets the old x) destroys information and blocks inversion at that point.So the invertible programs are exactly the deterministic, information-preserving ones — those that compute a one-to-one mapping from initial to final states. For such programs, S ; S⁻¹ is the identity and, symmetrically, S⁻¹ ; S is too, so the inverse of the inverse is the original: (S⁻¹)⁻¹ = S.
The power of the technique is that inversion is compositional: to invert a program, invert each of its parts and reassemble them. The rules below are the whole toolkit — there is one per construct in the language.
| Construct | Inverse | Note |
|---|---|---|
skip | skip⁻¹ = skip | Doing nothing is undone by doing nothing. |
S1 ; S2 | (S1 ; S2)⁻¹ = S2⁻¹ ; S1⁻¹ | Reverse the order, invert each step — undo the last thing first, like taking off shoes then socks. |
x := e | invertible only if e lets you recover the old x | See the discussion below — this is where information is usually lost. |
if … fi | invert each branch; guards must be reconstructable from the post-state | You must be able to tell, after the fact, which branch ran. |
do B → S od | a loop running S⁻¹ the same number of times | Needs a backward stopping test — a “co-guard.” |
The order flip is the rule people forget. If the forward program does A then B, its inverse does B⁻¹ then A⁻¹. This is forced: B ran last against the state A left, so B⁻¹ is the only thing that can restore that intermediate state, and only then can A⁻¹ restore the original.
# forward: x := x + 1 ; x := x * 2
# inverse: x := x / 2 ; x := x - 1 (reversed order, each step inverted)
# check: start x=5 → +1 → 6 → *2 → 12 → /2 → 6 → -1 → 5 ✓An assignment x := e is invertible only when the expression e lets you compute the old value of x back from the new one. The invertible cases are exactly the reversible arithmetic ones.
# add a constant → subtract it
x := x + c inverse: x := x - c
# double → halve (only if division is exact)
x := x * 2 inverse: x := x / 2
# negate → negate
x := -x inverse: x := -x# overwrites x with a constant:
# the old x is gone forever
x := 5
# unless the old value was saved first:
old := x ; x := 5
# inverse: x := old (now recoverable)The lesson: x := e is invertible when e depends on the old x in a one-to-one way. x := x + c and x := x * 2 (with exact division) qualify; x := 5 does not, because after it runs the old x is unrecoverable. Saving the old value first — old := x — restores invertibility, at the cost of extra state.
To invert an alternative command, invert each branch. But there is a catch the assignment case did not have: after the command runs, you must be able to tell which branch was taken, purely from the post-state. Each forward guard Bi needs a matching post-guard that is true exactly when branch i ran.
# forward
if x < 0 → x := x + 100
[] x ≥ 0 → x := x + 200
fi
# after branch 1: x is in [100,199]; after branch 2: x ≥ 200
# the ranges do not overlap → the branch taken IS recoverable
# inverse: guard on the post-state, undo the matching branch
if x < 200 → x := x - 100
[] x ≥ 200 → x := x - 200
fiIf two branches could leave the state in overlapping conditions, the post-guards cannot be written and the IF is not invertible — that overlap is precisely information loss (you can no longer tell which path produced the result).
The inverse of a loop is another loop. If the forward loop do B → S od executes its body n times, the inverse must execute S⁻¹ exactly n times — no more, no fewer. The difficulty is knowing when to stop going backward. The forward guard B tells you when to keep going forward; the inverse needs its own test — a co-guard BB that is true on every state the forward loop passed through and becomes false exactly when you reach the original starting state.
# forward loop, body run n times
do B → S od
# inverse loop: run S⁻¹ the same n times, stop via the co-guard BB
do BB → S⁻¹ odChoosing BB is the real work of inverting a loop: it must fire the inverse body precisely n times. Often a counter or a monotone quantity from the loop gives it to you directly (as in the worked example below, where the co-guard is simply i ≠ 0).
Inversion is not a curiosity. It shows up wherever “go back” or “the other direction” is a real requirement.
k-subset of {0..n-1}), computes its rank — its position in the standard ordering of all such combinations. Going the other way — given a rank, produce the corresponding combination (“unranking”) — looks harder. But the ranking program is invertible, so you do not design the unranker separately: you invert the ranker. The inverse reads a rank and reconstructs the combination that produced it, and it is correct because inversion preserves the specification.Take a simple loop that walks a counter forward, accumulating as it goes, and derive its inverse mechanically. Forward, we start at i = 0 and count up to n, adding i into a running sum:
# pre: i = 0 and s = 0
# post: i = n and s = 0+1+...+(n-1)
i := 0 ; s := 0 ;
do i ≠ n →
s := s + i ;
i := i + 1
od# pre: i = n and s = 0+1+...+(n-1)
# post: i = 0 and s = 0
# co-guard: i ≠ 0 (loop back exactly n times)
do i ≠ 0 →
i := i - 1 ;
s := s - i
odEvery piece of the inverse comes straight from the rules. The forward body is the sequence s := s + i ; i := i + 1; by the composition rule its inverse reverses the order and inverts each step, giving i := i - 1 ; s := s - i — and note the inner order matters, we must roll i back before subtracting so we subtract the same value that was added. The forward loop ran its body n times (until i = n); the co-guard i ≠ 0 makes the inverse run its body n times too, stopping exactly when i returns to 0.
Now the correctness claim {P} forward ; inverse {P}. Let P assert i = 0 ∧ s = 0. Running forward lands in the state i = n ∧ s = 0+1+…+(n-1). The inverse loop then subtracts each i back out in the reverse order it was added and decrements i each pass, terminating with i = 0 and s reduced back to 0 — exactly P. Trace it for n = 3:
# forward: (i,s): (0,0)→(1,0)→(2,1)→(3,3) s = 0+1+2 = 3
# inverse: (3,3)→ i=2,s=3-2=1 → i=1,s=1-1=0 → i=0,s=0-0=0
# back to (0,0) = P ✓Pulling the rules together, a program is invertible exactly when it destroys no information at any step. Concretely, three conditions must all hold.
x := x + c), or the old value was saved elsewhere first.| Construct | Invertible? | Because |
|---|---|---|
skip | Always | Changes nothing, so nothing to recover. |
x := x + c, x := -x | Yes | Old x recomputable from the new value. |
x := x * 2 | Yes, if exact | Halving recovers it, provided division is exact (no truncation). |
x := 5 (constant) | No | Old x overwritten and lost. |
x := x * 0, integer x := x / 2 | No | Many inputs map to one output — not one-to-one. |
S1 ; S2 | If both parts are | Inverse is S2⁻¹ ; S1⁻¹. |
if … fi | If branch is recoverable | Post-guards must identify the branch taken. |
do … od | If a co-guard exists | Must run the inverse body the same number of times. |
Nondeterministic S | Generally no | Same result reachable from many starts — ambiguous. |
| Idea | The one-line takeaway |
|---|---|
| What inversion is | S is invertible if some S⁻¹ gives {P} S ; S⁻¹ {P} — it undoes S. |
| Precondition | Only deterministic, information-preserving (one-to-one) programs can be inverted. |
skip and sequence | skip⁻¹ = skip; (S1;S2)⁻¹ = S2⁻¹ ; S1⁻¹ — reverse order, invert each. |
| Assignment | Invertible only if e recovers the old x: x:=x+c yes, x:=5 no. |
| Selection (IF) | Invert each branch; the branch taken must be recoverable from the post-state. |
| Iteration (DO) | Inverse is a loop running S⁻¹ the same number of times, stopped by a co-guard. |
| Why invert | Undo/redo, reversible computing, deriving a hard algorithm as the inverse of an easy one, enumeration. |
| Unranking example | Invert the rank-of-combination program to get combination-from-rank for free. |
| Invertibility test | No unrecoverable overwrite, guards recoverable, loops with a backward stop. |