Using Logic Programming to Test Module Specifications in Early Stages of Software Development

To build a complete software system, it is widely recognized that a proper decomposition of the system into modules can facilitate the software construction process. Such decomposition can be accomplished by modeling software modules as Abstract Data Types (ADTs). ADTs can be formally specified by using Bartussek and Parnas' TRACE. We investigate the feasibility and practicality of translating TRACE specifications into Prolog programs, keeping a TRACE-like format, in such a way that can actually be executed. Besides exercising the specification before any implementation, we can run both the actual implementation and the TRACE specification and then verify whether the implementation matches the specification. Additionally, we can partially avoid the maintenance of test-case databases as the specification itself will provide output according to a given input. An experiment has been carried out.