Extended Static Checking for JavaCormac Flanagan K. Rustan M. Leino∗Mark LillibridgeGreg Nelson James B. Saxe Raymie StataCompaq Systems Research Center 130 Lytton Ave. Palo Alto, CA 94301, USAABSTRACTSoftware development and maintenance are costly endeav-ors. The cost can be reduced if more software defects aredetected earlier in the development cycle. This paper in-troduces the Extended Static Checker for Java (ESC/Java),an experimental compile-time program checker that findscommon programming errors. The checker is powered byverification-condition generation and automatic theorem-proving techniques. It provides programmers with a sim-ple annotation language with which programmer design de-cisions can be expressed formally. ESC/Java examines theannotated software and warns of inconsistencies between thedesign decisions recorded in the annotations and the actualcode, and also warns of potential runtime errors in the code.This paper gives an overview of the checker architecture andannotation language and describes our experience applyingthe checker to tens of thousands of lines of Java programs.Categories and Subject DescriptorsD.2.1 [Software Engineering]: Requirements/Specifications;D.2.4 [Software Engineering]: Program VerificationGeneral TermsDesign, Documentation, VerificationKeywordsCompile-time program checking1. INTRODUCTIONOver the last decade, our group at the Systems ResearchCenter has built and experimented with two realizations ofa new program checking technology that we call extended∗Current address: Microsoft Research, One Microsoft Way,Redmond, WA 98052.Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies arenot made or distributed for profit or commercial advantage and that copiesbear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.PLDI’02, June 17-19, 2002, Berlin, Germany.Copyright 2002 ACM 1-58113-463-0/02/0006 ...$5.00.coverageefforttypecheckingextendedstaticcheckingprogramverificationdecidability ceilingFigure 1: Static checkers plotted along the two di-mensions coverage and effort (not to scale).static checking (ESC): “static” because the checking is per-formed without running the program, and “extended” be-cause ESC catches more errors than are caught by conven-tional static checkers such as type checkers. ESC uses anautomatic theorem-prover to reason about the semantics ofprograms, which allows ESC to give static warnings aboutmany errors that are caught at runtime by modern program-ming languages (null dereferences, array bounds errors, typecast errors, etc.). It also warns about synchronization er-rors in concurrent programs (race conditions, deadlocks).Finally, ESC allows the programmer to record design de-cisions in an annotation language, and issues warnings ifthe program violates these design decisions. Our first ex-tended static checker, ESC/Modula-3, has been describedelsewhere [8]. This paper provides an overview of our sec-ond checker, ESC/Java. It is not our goal in this paperto give a complete description of ESC/Java, but rather togive an overview that includes citations to more completedescriptions of particular aspects of the checker.Static checking can improve software productivity becausethe cost of correcting an error is reduced if it is detectedearly. Figure 1 compares ESC with other static checkers ontwo important dimensions: the degree of error coverage ob-tained by running the tool and the cost of running the tool.In the upper right corner is full functional program verifica-tion, which theoretically catches all errors, but is extremelyexpensive. In the lower left corner are static checking tech-niques that are widely used, which require only modest ef-fort, but catch only a limited class of errors: conventionaltype checkers and type-checker-like tools such as lint [23].These two corners of Figure 1 exercise a magnetic fascina-tion on programming researchers, but we suggest that the234middle of the diagram is promising, and it is there that weposition ESC: we hope to produce a cost-effective tool bycatching more errors than a type system or lint-like tool ata cost much less than full functional program verification.The horizontal line in Figure 1 labeled the “decidabilityceiling” reflects the well-known fact that the static detec-tion of many errors of engineering importance (includingarray bounds errors, null dereferences, etc.) is undecidable.Nevertheless, we aim to catch these errors, since in our en-gineering experience, they are targets of choice after typeerrors have been corrected, and the kinds of programs thatoccur in undecidability proofs rarely occur in practice. Tobe of value, all a checker needs to do is handle enough simplecases and call attention to the remaining hard cases, whichcan then be the focus of a manual code review.A distinguishing feature of our work is that ESC/Modu-la-3 and ESC/Java both perform modular checking: that is,they operate on one piece of a program at a time—it is notnecessary to have the source of the whole program in orderto run the checker. In our case, a “piece” is a single routine(method or constructor). Whether an automatic checker ormanual checking like code reviews is used, modular checkingis the only checking that scales. Consequently we considermodular checking to be an essential requirement.The cost of modular checking is that annotations are need-ed to provide specifications of the routines that are calledby the routine being checked. We argue that, in the absenceof an automatic checker, manual checking depends on thesesame annotations, typically in the form of English comments(which, not being machine checkable, easily get out of synchwith the source code over the life of a program). Unlikethe complicated predicate logic specifications that seem tobe required for full functional verification, ESC annotationsare straightforward statements of programmer design deci-sions. Indeed, we are excited about the prospect that theuse of ESC in the classroom may help in the notoriouslydifficult job of teaching students to write good comments,since ESC is a practical tool that gives error messages of theform “missing comment” and “inaccurate comment”.Two attributes of an ideal static checker are (1) if theprogram has any errors