← CatZep/Engineering Guides/The Science of Programming
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.
Student edition · understand, apply, verify
Understand reversible mappings on explicit domains and why overwritten information may prevent undo.
What you should be able to do: Define an inverse on reachable output states, preserve required history, and reject unsupported outputs.
Assumes basic programming, not formal-methods notation. This guide defines the needed notation locally. Scalar proofs use mathematical integers unless stated otherwise; finite arrays require integer valid bounds. Guarded-command notation is not Python syntax. Machine overflow, floats, exceptions, aliasing, and concurrency need additional contracts.
{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.Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.
An inverse recovers an earlier state only when the forward operation preserves enough information. Many-to-one mappings cannot have a unique inverse without extra data.
Example. x:=x+3 inverts to x:=x−3 over integers. x:=0 discards the old x.
Boundary. Rounding, overwrites, branch choices, and deletes can lose information. Inverses need domain/range and termination conditions.
A precondition states required inputs/state before an operation. A postcondition states the result promised when those requirements hold and execution terminates normally. Together they make requirements testable.
Example. For sum_first(b,n), require integer 0≤n≤len(b) and numeric elements; promise the sum of b[0:n].
Boundary. State exceptions, mutation, numeric domains, and empty cases. A mathematical array range does not automatically validate a runtime input.
Aliasing means multiple names refer to one mutable object. A frame condition specifies state the operation leaves unchanged.
Example. A sorted-copy function promises it does not mutate its input. Two swap parameters may unexpectedly name one location.
Boundary. State ownership, shared references, mutation, and exception behavior. Local-variable reasoning alone does not protect aliased global state.
A variant strictly decreases each iteration in a well-founded order. A natural-number variant cannot decrease forever while remaining nonnegative.
Example. An array scan uses n−i; repeated subtraction division uses remaining dividend.
Boundary. A positive real can halve forever. Use discrete domains or another well-founded order; nested loops need a correct combined or lexicographic bound.
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.
Specify a forward domain D, a reachable output range f(D), and the state you require restored. A deterministic one-to-one mapping f has a mathematical inverse on its image; a program inverse must also be computable and terminating under its input precondition. A two-sided identity is only asserted on the appropriate domain/range.
Do not conclude 'invertible exactly when deterministic' in every relational model. Nondeterministic outputs can sometimes retain enough information to recover the unique permitted starting state; conversely deterministic overwrites can lose it. The relevant property is recoverability under the actual state/model.
Scratch/history is state too. Saving old x can recover x, but overwriting a prior scratch value does not restore the whole prior machine state unless the frame excludes it or history preserves it. Ordinary undo is often a compensating history operation, not a mathematical inverse of every external effect.
For invertible component mappings, undo in reverse order: inverse(S1;S2)=inverse(S2);inverse(S1), with compatible intermediate domains. Addition by a constant can invert by subtraction under an exact arithmetic contract. Doubling is invertible on its reachable even integer outputs; truncating division usually loses information.
For selection, determine which inverse branch is valid from reachable output state or saved branch history. For x<0 map to x+100; for x≥0 map to x+200. The first range is y<100, not [100,199]; the second is y≥200. The gap 100≤y<200 is unreachable and should be rejected by a total runtime interface.
def inverse_piecewise(y):
if type(y) is not int:
raise ValueError('integer required')
if y < 100:
return y - 100
if y >= 200:
return y - 200
raise ValueError('outside the forward image')An inverse loop needs enough state/history and a backward stopping rule to recover exactly the permitted starting state. Merely reversing statements does not reveal how many iterations occurred. Lost information must be recorded or the contract restricted.
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 ✓Check recoverable inputs, reachable output precondition, exact numeric semantics, side effects/frame, branch history, and termination of forward/inverse programs. One-to-one mathematical mappings do not automatically make every runtime value a supported inverse input.
Overwrites, rounding, lossy compression, many-to-one operations, and external actions may need retained history or new corrective operations. 'Undo is free' is incorrect: history, computation, resource state, and external effects cost work and may not be reversible.
Work through the state changes and the exact claim being checked.
| Step | Evidence, decision, and expected result |
|---|---|
| Choose the forward mapping | For integer x<0 return x+100; for x≥0 return x+200. |
| Compute reachable ranges | First branch outputs values <100; second outputs values ≥200. Outputs 100 through 199 are unreachable. |
| Invert only reachable outputs | For y<100 return y−100; for y≥200 return y−200; reject the gap. |
| Define state scope | Saving old x in scratch can recover x, but may overwrite the prior scratch value. Claim restoration only for the specified state/frame or retained history. |
No. A one-to-one function has an inverse on its image; a two-sided identity requires the appropriate domain/range and a computable terminating inverse.
Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:
python3 guide_labs.py inversion
python3 guide_labs.py testThe complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.
The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.
| 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. |