Presentation: "User-defined type systems for error detection and prevention"
Time: Friday 13:00 - 14:00
Location: Cornell
Types help to detect and prevent errors: types help programmers to organize and document data, and types allow tools to verify that a program does not violate the type system's constraints. However, there is often much information about a type that a programmer cannot express. User-defined type qualifiers can enrich the built-in type system, permitting more expressive compile-time checking and guaranteeing the absence of certain errors. Examples of type qualifiers are NonNull, ReadOnly, Interned, and Tainted.
We have created a framework for Java that a type system designer to define new type qualifiers, and to create compiler plug-ins that check their semantics and issue lint-like warnings. A programmer can then use these type qualifiers throughout a program to obtain additional guarantees about the program. Developers can create and use the type qualifiers that are most appropriate for their software. Our toolset is fully backward-compatible with Java 5 annotations (and even with pre-annotations Java 4). Type annotations are scheduled for full support in Java 7, as part of JSR 308.
In the talk, I will present case studies of 4 checkers for type qualifiers. Each one found errors in real software, and is freely available for download. I will also discuss how you can create your own type qualifiers and checkers.