A theory of black-box testing in which the test-selection problem is given a mathematical statement: a program P is correct with respect to an algebraic specification SP when P, viewed as a Sigma-algebra, satisfies the axioms of SP. The exhaustive test set Exhaust(SP) is the set of ground instances of those axioms; it is generally infinite, so practical testing reduces it under explicitly stated selection hypotheses -- uniformity hypotheses (if the program is correct on one representative of a subdomain it is correct on the whole subdomain) and regularity hypotheses (correctness up to a bounded term complexity implies correctness in general). Unfolding procedures split an axiom's ground instances into subdomains by case analysis over the specification, yielding a finite practicable test set together with a precise record of the assumptions under which it is exhaustive. The framework also confronts the oracle problem for encapsulated data types: equalities between non-observable sorts cannot be decided directly, so correctness is weakened to observational or behavioural correctness, judged through minimal observable contexts, and the resulting testability hypotheses (H-min and its constrained variants) are made part of the test method rather than left implicit.
An algebraic specification defines an abstract data type by a signature (a set of sorts and of operation profiles) together with axioms - positive conditional equations relating the operations - so t…