Treffer: CJC: An Extensible Checker for the CleanJava Annotation Language

CleanJava is a formal annotation language for the Java programming language to support a Cleanroom-style functional program verification technique that views programs as mathematical functions. It needs a suite of support tools including a checker that can parse annotations and check them for syntactic and static semantic correctness. The two key requirements of the checker are flexibility and extensibility. Since the language is still under development and refinement, it should be flexible to facilitate language experimentation and accommodate language changes. It should be also extensible to provide base code for developing more advanced support tools like an automated theorem prover. In addition, it should recognize Java syntax, as CleanJava is a superset of Java. In this paper we describe our experience of developing a CleanJava checker called CJC and explain how we met the above requirements by using an open-source Java compiler. We expect our techniques and the lessons that we learned be useful to others implementing Java-like languages.