CJC: An extensible checker for the CleanJava annotation language

Formal program verification can be used as a complementary technique to software testing. It allows checking the correctness of all the states of a program which may be impossible using only software testing as a verification technique. One software development process that relies on formal verification is Cleanroom Software Engineering. Cleanroom\u27s main principles are to certify the software with respect to its specification and to produce zero-fault or near-zero-fault software. Cleanroom has being tested primarily in safety-critical systems that require a high level of correctness by development teams in places such as NASA and IBM, demonstrating lower fault rates and improved reliability. One of the techniques derived from Cleanroom is functional program verification. Functional program verification consists of calculating the function computed by the code (code function) and comparing it with its formal specification (intended function). A program is correct with respect to its specification if both functions are equivalent. CleanJava is a formal annotation language for the Java language that supports Cleanroom-style functional program verification. CleanJava has two main purposes: to promote the use of functional program verification (especially in the academia) and to serve as a platform for the development of techniques and tools that enable automatic or semi-automatic functional program verification. Currently there are no support tools for the CleanJava language. The main step towards building CleanJava tools is the creation of a language checker that parses CleanJava specifications and performs static analysis such as syntax and type checking on those specifications. However, developing a checker for CleanJava poses several interesting challenges. The checker needs to be sufficiently flexible and extensible since the CleanJava language is still under development requiring constant experimentation and implementation of new language features. The checker will serve as a base platform to more advanced tools such as fully automated theorem provers, so it needs to support extension mechanisms and integration with other development tools. Because CleanJava notation is based on the Java language syntax and CleanJava annotations are embedded in Java programs, the checker needs to understand and process Java code as well. This would require building yet another Java compiler or ideally extending an existing Java compiler. In this thesis I describe a series of solutions to address the above mentioned challenges related to developing a CleanJava checker (CJC). A key element in my solutions is to implement the CJC tool as an extension of an existing Java compiler that provides extensibility features. JastAddJ was used as the base code to support extensibility and avoid building a new Java compiler. JastAddJ is an extensible Java compiler that allows creating Java language extensions in a modular way. JastAddJ extensibility capabilities are provided by JastAdd, a meta-compilation system for creating modular and extensible compilers. Another key element in my solution approach was to build a set of tools that facilitate the creation of CleanJava language features including JastAdd specification file generators using XML templates. The current implementation of CJC supports most of the CleanJava language features and can be used as an alternative to a Java compiler such as javac