We propose a test case selection methodology for object-oriented software. This methodology is based on formal specifications and is aimed at verifying the correctness of method interaction of an object or a cluster of objects. The essence of this methodology is to select test cases by a reduction process. The exhaustive test set, the reference for correctness, is transformed into a practicable test set by applying hypotheses to the objects. We present a set of hypotheses specific to object-oriented systems. Regularity hypotheses are m:n generalizations of the unit behaviour and provides for specifying the shape of test cases. Uniformity hypotheses are 1:n generalizations. Used in conjunction with subdomain decomposition, they guarantee a coverage of the specification. Incrementallity hypotheses take advantage of the subtyping and subclassing relationships to justify the reuse of test cases.