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)
    49 Downloads (Pure)

    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 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 (ACM)
    Pages8:1-8:6
    Number of pages6
    ISBN (Print)978-1-60558-540-6
    DOIs
    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
    http://software.imdea.org/~ab/FTfJP09/ftfjp09.html

    Publication series

    Name
    PublisherACM

    Workshop

    Workshop11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009
    Abbreviated titleFTfJP
    CountryItaly
    CityGenua
    Period5/07/095/07/09
    Internet address

    Keywords

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

    Cite this