Essay: Notes on Structured Programming

Overview
Edsger Dijkstra’s 1970 essay “Notes on Structured Programming” argues that programming must be treated as a disciplined, mathematical activity whose primary aim is to produce correct programs that can be understood and maintained. He confronts the rising complexity of software and proposes structural constraints on program construction so that correctness can be established by design rather than by after-the-fact debugging. The essay crystallizes a methodology that ties program text, its intended behavior, and a humanly tractable proof of correctness into a single coherent artifact.

Programming as a Mathematical Discipline
Dijkstra promotes the view that a program is a proof-like object. A specification, stated with explicit preconditions and postconditions, is the starting point; the program is shaped so that its logic makes those assertions true. He criticizes reliance on testing as a primary means of validation, noting that tests can reveal faults but cannot guarantee their absence. The appropriate goal is derivation of programs whose correctness is demonstrable through formal reasoning. This stance leads to a style of programming that avoids opaque tricks and favors simplicity, clarity, and local verifiability.

Structure over Goto
A central polemic targets unstructured control transfer via the goto statement. While Böhm and Jacopini had shown that arbitrary control flow can be represented with just sequence, selection, and iteration, Dijkstra insists on the practical necessity of restricting ourselves to such structured constructs to keep the intellectual load manageable. He advocates single-entry, single-exit blocks nested to create a hierarchy matching the program’s logical decomposition. Eliminating arbitrary jumps enables the program text to mirror the proof structure, making correctness obligations local and comprehensible.

Blocks, Procedures, and Recursion
The essay embraces block structure and lexical scoping, as popularized by ALGOL, to confine detail and support abstraction. Procedures (including recursive ones) are presented as vehicles for both reuse and proof modularity: each procedure carries its own specification, and reasoning about a caller can proceed by treating the callee as an abstract operation that satisfies its contract. This layered view yields a program hierarchy where each level hides lower-level detail behind well-defined interfaces.

Stepwise Refinement
Dijkstra prescribes deriving programs through successive refinement. Begin with a simple outline that achieves the specification in principle, then replace abstract steps with more concrete ones, preserving correctness at each step. Each refinement is small enough to be reasoned about, and the cumulative effect is a program whose structure documents the path from specification to implementation. The method combats combinatorial explosion by ensuring that complexity is introduced in controlled, verifiable increments.

Invariants and Termination
A key proof technique is the use of assertions, especially loop invariants, to tie control structures to logical obligations. Before a loop, the invariant must be established; it must be maintained by the body; and after termination it must, together with the loop’s exit condition, imply the postcondition. For termination, Dijkstra advocates providing a variant (a quantity that decreases with each iteration under a well-founded order), ensuring that progress is demonstrable and infinite regress is excluded. Assertions strategically placed at block boundaries and before and after critical statements turn the program into a chain of small proofs.

Human Factors and Style
The discipline is motivated by human cognitive limits. Program text should be written to aid reasoning: clarity over cleverness, small scopes, and explicit contracts. Documentation is not an afterthought but inherent in the structured form and assertions of the program itself. The style fosters reliability and maintainability because future readers can reconstruct the argument for correctness from the code.

Legacy
“Notes on Structured Programming” reshaped programming practice by linking program design with formal reasoning, rejecting unstructured control, and championing stepwise refinement, block structure, and assertion-based correctness. Its core message endures: structure programs so that a simple, transparent proof of correctness is not only possible but natural.