Vladimir Glina and Stephen H. Edwards. Using wrappers to add run-time verification capability to Java Beans. In SAVCBS 2004: Specification and Verification of Component Based Systems, Technical Report #04-09, Dept. of Computer Science, Iowa State University, Ames, IA, August 2004, pp. 122-125.

Because of limited information exchange between component providers and users, both these parties should perform component verification. Java Modeling Language, a notation which allows writing of behavioral specifications for Java programs, can be used for verification purposes. This paper shows that placing JML specifications in separate wrappers distributed in the binary form alongside components gives component buyers an additional value. The wrapper can serve for Java components verification on the user’s side, verification checks can be enabled and disabled on per-class or per-package basis at run-time, and there is no performance overhead when they are disabled, unlike the traditional variant when checking code generated from JML specifications is placed directly into the underlying class bytecode. The paper describes wrapper design for Java Beans runtime verification and discusses advantages and challenges of it.