Purity and Side Effect Analysis for Java Programs

@incollection{salcianu05purity, abstract = {We present a new purity and side effect analysis for Java programs. A method is pure if it does not mutate any location that exists in the program state right before the invocation of the method. Our analysis is built on top of a combined pointer and escape analysis, and is able to determine that methods are pure even when the methods mutate the heap, provided they mutate only new objects. Our analysis provides useful information even for impure methods. In particular, it can recognize read-only parameters (a parameter is read-only if the method does not mutate any objects transitively reachable from the parameter) and safe parameters (a parameter is safe if it is read-only and the method does not create any new externally visible heap paths to objects transitively reachable from the parameter). The analysis can also generate regular expressions that characterize the externally visible heap locations that the method mutates. We have implemented our analysis and used it to analyze several applications. Our results show that our analysis effectively recognizes a variety of pure methods, including pure methods that allocate and mutate complex auxiliary data structures.}, author = {S\u{a}lcianu, Alexandru and Rinard, Martin }, citeulike-article-id = {2943158}, journal = {Verification, Model Checking, and Abstract Interpretation}, keywords = {design-by-contract, java, purity-analysis, softnet, static-analysis}, pages = {199--215}, posted-at = {2008-06-30 07:34:33}, priority = {2}, title = {Purity and Side Effect Analysis for Java Programs}, url = {http://www.springerlink.com/content/hrgarn1y96eafh1p }, year = {2005} }

TY - CHAP ID - salcianu05purity L3 - citeulike-article-id:2943158 TI - Purity and Side Effect Analysis for Java Programs JF - Verification, Model Checking, and Abstract Interpretation SP - 199 EP - 215 N2 - We present a new purity and side effect analysis for Java programs. A method is pure if it does not mutate any location that exists in the program state right before the invocation of the method. Our analysis is built on top of a combined pointer and escape analysis, and is able to determine that methods are pure even when the methods mutate the heap, provided they mutate only new objects. Our analysis provides useful information even for impure methods. In particular, it can recognize read-only parameters (a parameter is read-only if the method does not mutate any objects transitively reachable from the parameter) and safe parameters (a parameter is safe if it is read-only and the method does not create any new externally visible heap paths to objects transitively reachable from the parameter). The analysis can also generate regular expressions that characterize the externally visible heap locations that the method mutates. We have implemented our analysis and used it to analyze several applications. Our results show that our analysis effectively recognizes a variety of pure methods, including pure methods that allocate and mutate complex auxiliary data structures. KW - design-by-contract KW - java KW - purity-analysis KW - softnet KW - static-analysis AU - Sălcianu, Alexandru AU - Rinard, Martin PY - 2005/// UR - http://www.springerlink.com/content/hrgarn1y96eafh1p ER -