T.: Practical enforcement and testing of pluggable type systems

Pluggable type systems have been proposed in order to allow pro-grammers to easily extend a programming language’s type system to enforce new properties of interest. In previous work we pre-sented an approach to supporting pluggable type systems along with an instantiation of the approach for Java, called JAVACOP. This paper evaluates JAVACOP as a practical software development tool. We describe our experiences developing and using four dif-ferent checkers with JAVACOP. The first two checkers illustrate JAVACOP’s ability to enforce domain-specific properties of two different Java libraries, the Polyglot extensible compiler and the JUnit unit-testing framework. The other two checkers illustrate JAVACOP’s ability to express advanced type systems, respectively for enforcing non-null and unique object references. Using these checkers as motivation, we also describe two extensions to JAVA-COP that resolve earlier practical limitations: the ability to easily employ dataflow information in JAVACOP checkers, and the ability to test a JAVACOP checker against both the expected static disci-pline and a set of expected runtime invariants. 1