Structured programming and formal specification

In the author´s view structured programming consists of the use of the following: structure, abstraction, and specification. The purpose of this paper is to develop formal specifications for a nontrivial program in order to facilitate a proof of correctness. It is shown how the specifications serve as an abstraction for the program. A proof of correctness then consists of merely showing that the program at each level meets its formal specifications. Under this methodology lower levels of the program can be changed without affecting higher levels.