Software testing based on formal specifications: a theory and a tool

This paper addresses the problem of constructing test data sets from formal specifications. Starting from a notion of an ideal exhaustive test data set, which is derived from the notion of satisfaction of the formal specification, we show how to select by refinements a practicable test set, i.e. computable, while not rejecting correct programs (unbiased) and accepting only correct programs (valid), when assuming certain hypotheses. The hypotheses play an important role; they formalise common test practices and they express the gap between the success of the test and correctness; the size of the test set depends on the strength of the hypotheses. The paper shows an application of this theory for algebraic specifications and presents the actual procedures used to mechanically product such test sets, using Horn clause logic. These procedures are embedded in an interactive system, which, given some general hypothesis schemes and an algebraic specification, produces a test set and the corresponding hypotheses.