Static analysis of class invariants in Java programs.

详细信息   

• 作者：Bonilla-Quintero ; Lidia Dionisia.
• 学历：Doctor
• 年：2011
• 导师：Boyland,John,eadvisor
• 毕业院校：The University of Wisconsin
• ISBN：9781124738055
• CBH：3462830
• Country：USA
• 语种：English
• FileSize：3797322
• Pages：95

文摘

This paper presents a technique for the automatic inference of class invariants from Java bytecode. Class invariants are very important for both compiler optimization and as an aid to programmers in their efforts to reduce the number of software defects. We present the original DC-invariant analysis from Adam Webber,talk about its shortcomings and suggest several different ways to improve it. To apply the DC-invariant analysis to identify DC-invariant assertions,all that one needs is a monotonic method analysis function and a suitable assertion domain. The DC-invariant algorithm is very general； however,the method analysis can be highly tuned to the problem in hand. For example,one could choose shape analysis as the method analysis function and use the DC-invariant analysis to simply extend it to an analysis that would yield class-wide invariants describing the shapes of linked data structures. We have a prototype implementation: a system we refer to as "the analyzer" that infers DC-invariant unary and binary relations and provides them to the user in a human readable format. The analyzer uses those relations to identify unnecessary array bounds checks in Java programs and perform null-reference analysis. It uses Adam Webbers relational constraint technique for the class-invariant binary relations. Early results with the analyzer were very imprecise in the presence of "dirty-called" methods. A dirty-called method is one that is called,either directly or transitively,from any constructor of the class,or from any method of the class at a point at which a disciplined field has been altered. This result was unexpected and forced an extensive search for improved techniques. An important contribution of this paper is the suggestion of several ways to improve the results by changing the way dirty-called methods are handled. The new techniques expand the set of class invariants that can be inferred over Webbers original results. The technique that produces better results uses in-line analysis. Final results are promising: we can infer sound class invariants for full-scale,not just toy applications.