Testing in top-down program development

A program design methodology is presented that advocates the synthesis of tests hand-in-hand with the design at every stage of program development and uses them for early detection of design flaws. It involves formal specifications of abstract programs and abstract data refinement that appear in the design. The main findings are: (1) formalization facilitates black-box and design-based functional testing; (2) abstract data testing allows a more natural selection of tests than concrete data testing; (3) black-box testing leads to significant structural coverage testing; and (4) the method can be combined with formal verification