Extended static checking for Java

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