HFM2019

History of Formal Methods Workshop

Mark Priestley

The early history of flow diagrams as a formal method

In their first report on Planning and Coding Problems for an Electronic Computing Instrument, issued in 1947, Herman Goldstine and John von Neumann proposed a notation they called flow diagrams. These diagrams did not simply provide a graphical representation of the “control flow” in a program, but were part of a detailed and comprehensive approach intended to reveal “errors and omissions” in program plans.

Thanks to the preservation of a little-known draft version of the report and correspondence between Goldstine and von Neumann, the evolution of the notation can be traced in some detail. A persistent theme within the development was the attempt to find an adequate way of describing the behaviour of iterative loops in programs. I will trace the outline of this history, paying particular attention to those aspects of the notation that were used to check the correctness of the program being designed.

The Planning and Coding reports contain a number of textbook examples of the use of the notation, and in 1949 Alan Turing used a flow diagram to illustrate a process for “checking large routines”. A comparison of Turing’s diagram with the Goldstine/von Neumann notation reveals many similarities, but also a significant difference.

However, in practice the use of the notation moved away from an explicit concern with correctness. As far as we know, the first application of the notation “in the wild” was for the Monte Carlo programs run on ENIAC in early 1948. Examination of the flow diagrams produced for this project, some produced by von Neumann himself, show that the notation quickly evolved from its textbook form into a less detailed version that emphasized program structure at the expense of detailed annotation of the properties of data. The presentation will conclude by considering some factors that may have contributed to this change.


Priestley HFM 2019 Slides.pptx