On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)
    106 Downloads (Pure)


    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 languageUndefined
    Title of host publicationProceedings of the 11th International Workshop on Formal Techniques for Java-like Programs
    EditorsA. Banerjee
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery
    Number of pages6
    ISBN (Print)978-1-60558-540-6
    Publication statusPublished - 2009
    Event11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009 - Genua, Italy
    Duration: 5 Jul 20095 Jul 2009
    Conference number: 11

    Publication series



    Workshop11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009
    Abbreviated titleFTfJP
    Internet address


    • IR-68896
    • METIS-264235
    • EWI-16995
    • Semantics
    • run-time checker
    • finally clauses

    Cite this