Beyond one algorithm
Edsger Dijkstra is widely associated with shortest-path computation, but his work on concurrency, semaphores and structured programming was also influential. Precise reasoning about program behavior was a recurring concern.
A developer’s exercise
Before adding complexity, write down the assumptions and conditions under which the code is correct. Tests and reasoning complement each other; understanding why a program works matters alongside observing successful outputs.
Assumptions belong to the algorithm
Dijkstra’s shortest-path algorithm is often introduced through a graph and a few numbers. Its conditions matter just as much as the steps. In the usual formulation, edge weights must be nonnegative. Omitting that condition can apply a correct method to the wrong problem.
Ordinary software has similar preconditions. A function that relies on sorted input needs to state or enforce that requirement. Hidden assumptions can turn apparently reasonable inputs into incorrect outcomes.
Concurrency and reasoning about behavior
Concurrent execution is not determined only by the line order in one function. Multiple operations can access shared state in different orders. The design must identify valid states and the points requiring coordination. Adding locks without understanding those relationships can introduce other failures.
Two updates to a shared counter provide a small example. A test with one fixed execution order may always succeed, while another ordering loses an update. Reasoning about permitted states and testing boundary conditions complement each other.
IROSG learning perspective
Before implementing a small algorithm, record its input precondition, guaranteed result and an invariant that should remain true during execution. Design tests around those promises instead of relying only on well-behaved examples.
The aim is not to demand a formal proof for every routine application. It is to develop the habit of explaining why a program is expected to work. “It succeeded in several runs” and “we have an argument for the specified conditions” are useful but different kinds of evidence.
