Testing Ada Abstract Data Types Using Formal Specifications

The purpose of this paper is to present an experiment with formal methods for the black-box testing of reusable abstract data types (ADTs). We propose to test a family of software components by re-engineering a formal specification from an existing Ada implementation, using algebraic specifications. From this well-defined basis, we generate test sets automatically, by constructing an exhaustive set of formulae that prove the property preservations of a program with respect to its specifications, and by reducing this set to a finite size by applying reduction hypotheses. Once the selection of a finite test set has been performed, we show how to build the oracle, the decision procedure for the success or the failure of a test set. Finally, we discuss the advantages of test sets generated from the formal specification over those defined by a programmer, based on his intuitive understanding of the behavior of the ADT.