Inference of Reference Immutability

Abstract. Javari is an extension of Java that supports reference immutability constraints. Programmers write readonly type qualifiers and other constraints, and the Javari typechecker detects mutation errors (incorrect side effects) or verifies their absence. While case studies have demonstrated the practicality and value of Javari, a barrier to usability remains. A Javari program will not typecheck unless all the references in the APIs of libraries it uses are annotated with Javari type qualifiers. Manually converting existing Java libraries to Javari is tedious and error-prone. We present an algorithm for inferring reference immutability in Javari. The flow-insensitive and context-sensitive algorithm is sound and produces a set of qualifiers that typecheck in Javari. The algorithm is precise in that it infers the most readonly qualifiers possible; adding any additional readonly qualifiers will cause the program to not typecheck. We have implemented the algorithm in a tool, Javarifier...

• Type: Conference
• Year: 2008
• Where: ECOOP
• Authors: Jaime Quinonez, Matthew S. Tschantz, Michael D. Ernst
• Keywords: ECOOP 2008, Javari Type Qualifiers, Programming Languages, Reference Immutability, Type Qualifiers