Abstract
This paper discusses how a subtle interaction between the semantics of
Java and the implementation of the JML run-time checker can cause the
latter to fail to report errors. This problem is due to the
well-known capability of finally clauses to implicitly override
exceptions. We give some simple examples of annotation violations that
are not reported by the run-time checker because the errors are caught
within the program text; even without any explicit reference to
them. We explain this behaviour, based on the official Java Language
Specification. We also discuss what are the consequences of this
problem, and we sketch different solutions to the problem (by adapting
the implementation of the JML run-time checker, or by adopting a
slightly different semantics for Java).
| Original language | Undefined |
|---|---|
| Title of host publication | Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs |
| Editors | A. Banerjee |
| Place of Publication | New York |
| Publisher | Association for Computing Machinery |
| Pages | 8:1-8:6 |
| Number of pages | 6 |
| ISBN (Print) | 978-1-60558-540-6 |
| DOIs | |
| Publication status | Published - 2009 |
| Event | 11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009 - Genua, Italy Duration: 5 Jul 2009 → 5 Jul 2009 Conference number: 11 http://software.imdea.org/~ab/FTfJP09/ftfjp09.html |
Publication series
| Name | |
|---|---|
| Publisher | ACM |
Workshop
| Workshop | 11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009 |
|---|---|
| Abbreviated title | FTfJP |
| Country/Territory | Italy |
| City | Genua |
| Period | 5/07/09 → 5/07/09 |
| Internet address |
Keywords
- IR-68896
- METIS-264235
- EWI-16995
- Semantics
- run-time checker
- finally clauses