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)
30 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

Huisman, M. (2009). On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. In A. Banerjee (Ed.), Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs (pp. 8:1-8:6). [10.1145/1557898.1557906] New York: Association for Computing Machinery (ACM). https://doi.org/10.1145/1557898.1557906
Huisman, Marieke. / On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. editor / A. Banerjee. New York : Association for Computing Machinery (ACM), 2009. pp. 8:1-8:6
@inproceedings{e7379bbe1997451b9403a3b73a991c5c,
title = "On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker",
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).",
keywords = "IR-68896, METIS-264235, EWI-16995, Semantics, run-time checker, finally clauses",
author = "Marieke Huisman",
note = "10.1145/1557898.1557906",
year = "2009",
doi = "10.1145/1557898.1557906",
language = "Undefined",
isbn = "978-1-60558-540-6",
publisher = "Association for Computing Machinery (ACM)",
pages = "8:1--8:6",
editor = "A. Banerjee",
booktitle = "Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs",
address = "United States",

}

Huisman, M 2009, On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. in A Banerjee (ed.), Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs., 10.1145/1557898.1557906, Association for Computing Machinery (ACM), New York, pp. 8:1-8:6, 11th Workshop on Formal Techniques for Java-like Programs, FTfJP 2009, Genua, Italy, 5/07/09. https://doi.org/10.1145/1557898.1557906

On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. / Huisman, Marieke.

Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. ed. / A. Banerjee. New York : Association for Computing Machinery (ACM), 2009. p. 8:1-8:6 10.1145/1557898.1557906.

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

TY - GEN

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

AU - Huisman, Marieke

N1 - 10.1145/1557898.1557906

PY - 2009

Y1 - 2009

N2 - 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).

AB - 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).

KW - IR-68896

KW - METIS-264235

KW - EWI-16995

KW - Semantics

KW - run-time checker

KW - finally clauses

U2 - 10.1145/1557898.1557906

DO - 10.1145/1557898.1557906

M3 - Conference contribution

SN - 978-1-60558-540-6

SP - 8:1-8:6

BT - Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

A2 - Banerjee, A.

PB - Association for Computing Machinery (ACM)

CY - New York

ER -

Huisman M. On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. In Banerjee A, editor, Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. New York: Association for Computing Machinery (ACM). 2009. p. 8:1-8:6. 10.1145/1557898.1557906 https://doi.org/10.1145/1557898.1557906