Propagation of JML non-null annotations in Java programs

Maciej Cielecki, Jędrzej Fulara, Krzysztof Jakubczyk, Łukasz Jancewicz · 2006

Development of high quality code is notably difficult. Tools that help maintaining the proper quality of code produced by programmers can be very useful: they may increase the quality of produced software and help managers to ensure that the product is ready for the market. One of such tools is ESC/Java2, a static checker of Java Modeling Language annotations. These annotations can be used to ensure that a certain assertion is satisfied during the execution of the program, among the others - to ensure that a certain variable never has a null value. Unfortunately, using ESC/Java2 can be very troublesome and time-consuming for programmers, as it lacks a friendly user interface and a function that propagates annotations.We present CANAPA, a tool that can highly reduce time and effort of eliminating null pointer exceptions in Java code. This tool can automatically propagate JML non-null annotations and comes with a handy Eclipse plug-in. We believe that functionality of CANAPA will minimize the effort required to benefit from using the JML non-null checking.

Read the paper · More papers on PaperTik