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

A discussion is given on 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, it is shown 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 authors show an application of this theory for algebraic specifications and present the actual procedures used to mechanically produce 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