Robert W. Floyd (BOB)

In 1967 Floyd built on earlier work of Alan Perlis, Saul Gorn and John McCarthy for proving programs correct. He developed a notation, initially for flowcharts and later for real programs, that assigned conditions at each branch and entry point in the program. Some conditions related to the value of variables, and ensured that if these conditions were true upon entry then they could be proven true at exit. Other conditions proved a program would halt, by requiring that, at each step, some value would decrease that could not decrease indefinitely. Before this approach, ensuring that a program satisfies its specifications required testing with different data, examining the output, fixing bugs, and then trying it again. While sometimes effective, this debugging process could not test every possible situation. Errors were often found in large programs years after they had been put into production. Floyd’s mathematical analysis was the beginning of a long series of attempts by him and others to prove a program correct before it was released to users. His paper on this topic [3] was very influential and inspired Tony Hoare to develop a system known as Hoare triples that furthered this work.

Bob also invented many important practical algorithms. Best known are those that find the shortest paths through networks, compute the median of data, and render gray scale images with binary pixels using error diffusion—the Floyd-Steinberg algorithm.