Extended static checking for Java

TLDR

Software development and maintenance are costly, but detecting defects earlier can reduce costs. The paper introduces ESC/Java, an experimental compile‑time checker for Java that detects common programming errors, and outlines its architecture, annotation language, and application to large codebases. ESC/Java uses verification‑condition generation and automatic theorem proving, coupled with a simple annotation language, to analyze annotated Java code and warn of design inconsistencies and potential runtime errors. The authors applied ESC/Java to tens of thousands of lines of Java code, demonstrating its practical use and revealing its effectiveness in detecting errors.

Abstract

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theorem-proving techniques. It provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. ESC/Java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. This paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of Java programs.