Specifying Java frameworks using abstract programs

We propose a novel approach to specifying, documenting, and reasoning about object oriented frameworks. The novelty of our approach is in combining standard executable statements of a programming language (we choose Java as an example) with possibly nondeterministic specification constructs. A specification of the intended behavior given in this language can serve as a precise documentation for users of the framework and its extension developers. To illustrate the applicability of our method to specification of object oriented frameworks, we demonstrate how one can specify the Java Collections Framework which is a part of the standard Java Development Kit 2.0