| dc.description.abstract | Gradual typing provides the ability to safely mix untyped or dynamically typed code
with statically typed code while maintaining, within the statically typed portion, the guarantees
claimed by the static typing. It is motivated by the idea that different amounts of
typing are valuable at different times during a software projects development. Less typing
is useful at the prototyping stage, where requirements change frequently, and rapid development
is important. More typing is useful in more mature projects where maintenance,
documentation, and correctness become critically important. Gradual aims to enable a
project to gradually move from one side of this spectrum to the other.
Pluggable typing and pluggable typing frameworks aim to allow a language to support
many different type systems, that can be developed by type system designers and plugged
into the existing compiler infrastructure. The Checker Framework is built on the OpenJDK➋
Java compiler, and provides a framework to develop additional type systems that
can be applied to Java code. It has been tested and proven using many other type systems.
However, not all code will adopt all type systems, so a developer who wishes to check their
project with a given type system may still link against other components that are not
checked with that type system. Additionally, a developer may wish to adopt a new type
system, but be unwilling to spend the effort necessary to annotate all the existing code for
the new type system.
The gradual extension to the Checker Framework aims to improve type safety of partially
applied Checker Framework type systems, using gradual typing techniques. A prototype
was built, and the gradual nullness type system was designed to prove it.
Defining the checked-unchecked boundary is crucial. Even though the use case is limited
to individual files being either entirely annotated or entirely unannotated, because Java is
an object-oriented language with inheritance, many different boundary conditions present
themselves. This work analyses each boundary condition in detail, and presents options for
runtime tests to ensure that values crossing the boundary meet the static type requirements
on the other side. The nature of the tests, and the method of passing the static type to
the runtime environment is discussed.
This work presents the design of the prototype, implemented in the Checker Framework
and OpenJDK➋. It discusses the design of the OpenJDK➋ compiler, the Checker
Framework, and how they work together. It demonstrates how the abstract syntax tree
can be modified in order to effect insertion of the runtime tests. It discusses the specific
implementation details needed to implement each boundary condition runtime test in Java.
An evaluation of the prototype is completed looking at correctness, both through a set
of synthetic tests, and by inserting artificial errors into an existing real world program;
performance, by running configurations of real world programs designed to model the
motivating examples; and applicability, by comparing the gradual framework with other
options for improving type safety in partially annotated programs.
Related work on both gradual typing and pluggable typing are discussed. Final remarks
and future work concludes the work. | en |
