The Classification Tree Method provides a flexible basis for systematic testing. Traditionally the generation of a classification
tree has been entirely manual. This paper introduces a new approach that extracts predicates from the Z specification of an
operation and builds a Classification Tree from these predicates. It thus shows how the generation of a Classification Tree
may be semi-automated on the basis of a Z specification. The paper also defines the notion of the test context of a predicate
that determines when the value of this predicate is relevant. The test context is used to reduce the number of tests produced
from the Classification Tree.
Keywords Classification tree method - test automation - formal methods - Z notation