Verifying the Option Type with Rely-Guarantee Reasoning

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 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. CCS CONCEPTS • Software and its engineering → Software verification and validation.