Parameter reference immutability: formal definition, inference tool, and comparison

摘要

Knowing which method parameters may be mutated during a method’s execution is useful for many software engineering tasks. A parameter reference is immutable if it cannot be used to modify the state of its referent object during the method’s execution. We formally define this notion, in a core object-oriented language. Having the formal definition enables determining correctness and accuracy of tools approximating this definition and unbiased comparison of analyses and tools that approximate similar definitions.