← Back to System Internals

Documenting Programs & Historical Notes

Gries’ closing chapters make a quiet but radical point: the assertions you invented to prove a program correct are its best documentation — and they sit at the end of a lineage that runs Floyd → Hoare → Dijkstra → Gries, from “verify after” to “derive correct by construction.”

Assertions ARE the documentation

Ask what a comment is worth and you get an uncomfortable answer: a comment records what someone hoped the code did at the moment they wrote it. It is prose, unchecked, and it rots the instant the code beneath it changes. Gries’ whole method hands you something categorically better. The precondition, the postcondition, and above all the loop invariant are not decoration bolted on afterward — they are the very predicates the program was derived from. They state intent precisely, in the same logic the code obeys, and they are checkable.

That is the shift in status. The pre/postcondition pair is the contract: it tells a reader exactly what the code assumes and exactly what it promises, without their having to read the body. The invariant tells them the idea of the loop — the single fact that stays true across every iteration — which is the one thing raw code never reveals. These assertions are the most valuable documentation a program can carry precisely because they are the documentation the compiler, the test suite, and a proof can all hold you to.

How to document a loop

A loop is the hardest construct to read cold, because its meaning lives in what accumulates over many iterations, not in any single line. Gries’ prescription is exact: next to every loop, record four things — the precondition that holds on entry, the invariant that holds before and after each iteration, the bound function that proves it terminates, and the postcondition it establishes on exit. Those four are not optional annotations; they are the loop’s specification.

q = 0
r = a
# loop through items
while r >= b:
    r = r - b
    q = q + 1
# why does this compute a / b ?
# what stays true each pass?
# why does it stop? the reader
# must reverse-engineer all of it.

# pre  Q: a ≥ 0 and b > 0
q = 0
r = a
# invariant P: a = q*b + r  and  0 ≤ r
# bound     t: r        (t ≥ 0, t decreases)
while r >= b:          # guard B
    r = r - b
    q = q + 1
# post R: a = q*b + r  and  0 ≤ r < b

Read the two versions side by side. The left tells you the shape of the code you can already see. The right tells you the four things the code cannot tell you: what it needs (a ≥ 0, b > 0), the exact relationship it maintains (a = q*b + r ∧ 0 ≤ r), why it halts (r is a non-negative integer that strictly drops each pass), and what it delivers (0 ≤ r < b). Anyone can now verify the loop without running it — on exit, invariant plus negated guard (0 ≤ r and r < b) yields the postcondition directly. The same skeleton documents a summation loop: invariant s = (sum of A[0..i-1]) ∧ 0 ≤ i ≤ n, bound n - i, post s = sum of A[0..n-1].

Documentation guidelines

The discipline distills into a handful of rules. None are about volume — more comments is not better documentation. They are about recording the things the code genuinely cannot say for itself, and never the things it already says plainly.

Assertions as executable checks

Here the documentation stops being passive. The very predicate that proves a loop correct can be dropped into the running program as an assert — a runtime check that fails loudly the moment reality diverges from the proof. The invariant that lived in a comment becomes an executable guard against regression.

def divide(a, b):
    assert a >= 0 and b > 0        # pre Q
    q, r = 0, a
    while r >= b:
        assert a == q*b + r and r >= 0  # inv P
        r -= b
        q += 1
    assert a == q*b + r and 0 <= r < b  # post R
    return q, r

# property-based test: for ANY valid input
# the postcondition must hold. The oracle is
# the specification itself, not a table of
# hand-picked expected outputs.
def test_divide(a, b):        # a ≥ 0, b > 0
    q, r = divide(a, b)
    assert a == q*b + r
    assert 0 <= r < b
    # one predicate certifies every case

This is the bridge to modern practice. Design by contract (Eiffel, and the require/ensure/invariant constructs it inspired) is Gries’ pre/post/invariant triad promoted to first-class language features that execute. Property-based testing (QuickCheck, Hypothesis) uses the postcondition as an oracle across machine-generated inputs, so the specification checks thousands of cases you would never enumerate by hand. Neither replaces a proof — an assertion that never fires proves nothing about the paths it did not take, and tests still show only the presence of bugs. But the same predicate serves in three roles at once: it proves the code, documents the code, and guards the code against future change. That triple duty is the payoff.

Historical notes — the lineage

Gries did not invent this calculus; he synthesized and taught it. The closing notes trace a fifteen-year arc in which the field’s ambition shifted from checking a finished program to growing a correct one. Four papers carry the story.

The single most important movement across this table is the change in when correctness enters. Floyd and Hoare give you tools to verify after: write the program, then prove it meets its spec. Dijkstra and Gries invert this into derive correct by construction: let the spec and the emerging proof drive the code so it is right the first time. The bound function that Floyd introduced for termination survives untouched all the way to Gries — a reminder that the ideas accreted rather than replaced one another.

What to take away

Notation dates; the discipline does not. Few programmers today write do…od or compute a wp by hand, yet the habits of mind the calculus instills are exactly the ones that separate reliable code from hopeful code.

• Think in invariants. Before writing a loop, ask what single fact stays true across every iteration. If you cannot state it, you do not yet understand the loop — and neither will the next reader.
• Let the spec lead. Start from the pre/postcondition, not the body. Code chosen to satisfy a contract is correct by construction; code written first and specified later is a debugging exercise waiting to happen.
• Prove termination. Every loop needs a bound function — a quantity, bounded below, that strictly decreases. “It probably stops” is not an argument.
• Keep assertions as living documentation. The predicates that prove the program are its truest documentation and its best regression guard. Maintain them with the code, and they pay you back three times over.

Summary