Treffer: 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's 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 ...