InferringPropagatingAnnotationsExplanation

Verifying a program typically requires many of program annotations. Error messages produced by a program analysis tool, which indicate failed verification attempts, can be used to automate the generation and propagation of program annotations in code.

This approach is pursued in the Canapa tool (CieleckiFJJCSK06): Canapa uses the error messages of ESC/Java2 to infer and propagate non-null annotations. Canapa comes with an Eclipse plug-in.

In an attempt to further reduce the burden of annotation writing further, we have implemented an algorithm dedicated to the generation of "obvious" minimal preconditions to avoid not only null-pointer, but also array-out-of-bounds exceptions (see (BBC+06)). This algorithm re-uses the implementation of the wp-calculus. A possibility to improve the algorithm is to apply a simple analysis to identify possible class invariants.

Version: 2 Time: Fri Mar 28 17:25:03 2008 Author: dcochran (dcochran) IP: 193.1.132.32