Download: PDF, slides (PDF), slides (Google Slides), implementation.
“Verifying the option type with rely-guarantee reasoning” by James Yoo, Michael D. Ernst, and René Just. In ASE 2024: Proceedings of the 39th Annual International Conference on Automated Software Engineering, (Saramento, CA, USA), Oct. 2024.
Many programming languages include an implementation of the option type, which encodes the absence or presence of values. Incorrect use of the option type results in run-time errors, and unstylistic use results in unnecessary code. Researchers and practitioners have tried to mitigate the pitfalls of the option type, but have yet to evaluate tools for enforcing correctness and good style.
To address problems of correctness, we developed two modular verifiers that cooperate via a novel form of rely-guarantee reasoning; together, they verify use of the option type. We implemented them in the Optional Checker, an open-source static verifier. The Optional Checker is the first verifier for the option type based on a sound theory — that is, it issues a compile-time guarantee of the absence of run-time errors related to misuse of the option type. We then conducted the first mechanized study of tools that aim to prevent run-time errors related to the option type. We compared the performance of the Optional Checker, SpotBugs, Error Prone, and IntelliJ IDEA in over 1M non-comment, non-blank lines of code. The Optional Checker found 13 previously-undiscovered bugs (a superset of those found by all other tools) and had the highest precision at 93%.
To address problems of style, we conducted a literature review of best
practices for the option type. We discovered widely varying opinions about
proper style. We implemented linting rules in the Optional Checker and
discovered hundreds of violations of the style recommended by Oracle,
including in 11% of JDK files that use Optional. Some of
these were objectively bad code, and others reflected different styles.
Download: PDF, slides (PDF), slides (Google Slides), implementation.
BibTeX entry:
@inproceedings{YooEJ2024,
author = {James Yoo and Michael D. Ernst and Ren{\'e} Just},
title = {Verifying the option type with rely-guarantee reasoning},
booktitle = {ASE 2024: Proceedings of the 39th Annual International
Conference on Automated Software Engineering},
address = {Saramento, CA, USA},
month = oct,
year = {2024}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.