McDonald's Problem - An Example of Using Dijkstra's Programming Method

In this paper, we use Dijkstra's method of simultaneously developing a program and a proof of its correctness to solve the so-called McDonald's warehouse problem. The problem briefly is to read a card file and print an inventory report. Our interest in it stems from the fact that it requires sequentially processing the records of a file--a task common to a large class of problems. As we solve the problem, we illustrate how to rigorously introduce file input/output operations within the framework of Dijkstra's method. This aspect of the solution is intended to be a paradigm that is applicable to the above-mentioned class of problems. Our solution serves one other purpose. The McDonald's warehouse problem is often used to compare the effectiveness of different programming methodologies in developing programs that sequentially process files. As discussed in Ref. 1, the programs developed using the data structure design methodology are generally considered to be the most desirable. This is primarily because the structure of the resulting 2157