This work investigates the fundamental question of how to construct correct computer programs through rigorous mathematical derivation rather than trial-and-error testing. Edsger W. Dijkstra, a pioneer in computer science, collaborates with W. H. J. Feijen and Joke Sterringa to present a formal methodology for program development. The text argues that the logical structure of a program should be derived from its specification, utilizing the calculus of predicate transformers to ensure correctness by design. By shifting the focus from debugging to formal verification, the authors provide a systematic framework for reasoning about program behavior.

Experts recognize this text as a foundational contribution to the field of formal methods in computer science. Readers frequently note the high level of mathematical density and the rigorous, uncompromising nature of the prose.