VMCAI 2009


William C. Benton and Charles N. Fischer. Mostly-Functional Behavior in Java Programs. In Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI ’09). Savannah, Georgia, USA 18-20 January 2009. © Springer.


We present a lightweight type-and-effect system for Java programs that features two major innovations over extant object-oriented effects systems: initialization effects, which are writes to an object’s state while it is being constructed, and quiescing fields, which are fields that are never written after an object is constructed. We also present a novel taxonomy of degrees of method purity in object-oriented programs, which characterizes methods whose effects are confined to their receiver object. Finally, we find significant amounts of mostly-functional behavior in realistic Java programs: in the benchmarks we analyzed, between 48–53% of declared fields were identifiable as quiescing and between 24–78% of dynamic field reads were from quiescing fields.

Paper and talk

PDF (408kb), talk slides (396kb).