Conference paper

Testing of 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.

    Keywords: Paper ; Ada ; Testing ; Conform


    Also available as Technical Report EPFL-DI No 94/75


    • LGL-CONF-1994-002

    Record created on 2005-09-20, modified on 2016-08-08

Related material