McDonald's Problem-An Example of Using Dijkstra's Programming Method
D. K. Sharma · Bell System Technical Journal · 1981
We use Dijkstra's programming method to solve the so-called McDonald's problem and show how to rigorously introduce file input/output operations in the program. The steps involved are quite simple and the paradigm suggested is applicable to the wider class of problems that involve sequentially processing file records. For these problems, the programs developed using the data structure design methodology are generally considered to be the most desirable. We show that Dijkstra's method can yield the same program. Unlike other methodologies, it also yields a correctness proof, which is extremely valuable in understanding the program and in modifying it.