|This thesis presents the design, implementation, and evaluation of an extension to the Java language,
ConstJava, that is capable of expressing immutability constraints and verifying them at
compile time. The specific constraint expressed in ConstJava is that the transitive state of the
object to which a given reference refers cannot be modified using that reference.
In addition to the ability to specify and enforce this basic constraint, ConstJava includes several
other features, such as mutable fields, immutable classes, templates, and the const cast operator,
that make ConstJava a more useful language.
The thesis evaluates the utility of ConstJava via experiments involving writing ConstJava code
and converting Java code to ConstJava code. The evaluation of ConstJava shows that the language
provides tangible benefits in early detection and correction of bugs that would otherwise be difficult
to catch. There are also costs associated with the use of ConstJava. These are minimized by
ConstJavaís backward compatibility with Java, and by the high degree of inter-operability of the
two languages, which allows for a less painful transition from Java to ConstJava.
This technical report is a revision of the authorís Masterís thesis, which was advised by Prof. Michael