Specification directed module testing

If a program is developed from a specification in a mathematically rigorous manner, work done in the development can be utilized in the testing of the program. The better understanding afforded by these methods provides a more thorough check on the correct operation of the program under test. This should lead to earlier detection of faults (making it easier to determine their causes), more useful debugging information, and a greater confidence in the correctness of the final product. Overall, a more systematic approach should expedite the task of the program tester and improve software reliability. The testing techniques described here apply to the testing of abstract data types (modulus, packages). The techniques utilize information generated during refinement of a data type, such as the data type invariant and the relationship between the specification and implementation states; this information is used to specify parts of the code to be written for testing.