User-Defined Type Extensions
Type systems are a natural discipline for specifying
and statically checking properties of programs.
Researchers have shown how to extend
types in traditional type systems to check many different classes
of properties. For example, types have been used to statically ensure
memory safety in the presence of manual memory management, lack of
race conditions in the presence of multithreading, and proper
(non)aliasing in the presence of pointers.
Of course, language designers cannot anticipate all the properties
that programmers will want to specify and check. Language
designers also
cannot anticipate all of the practical ways in which types
may be used in order to enforce a particular property.
Therefore,
it is desirable to provide a framework for
user-defined type extensions, whereby programmers
can easily augment a language's type system in order
to ensure properties of interest.
Check out a 2-page overview of our approach
here.
[ Clarity
| JavaCOP
]
Clarity is a novel framework for user-defined type qualifiers,
which refine existing types, for C
programs. Clarity provides a declarative language in which users can
define new qualifiers along with rules that define the programming
discipline associated with each qualifier (e.g., a nonnull
pointer can safely be dereferenced).
An extensible typechecker employs these user-defined rules to
automatically check annotated C programs. Users may also provide an
explicit invariant for each qualifier, indicating the run-time
property that it is meant to ensure (e.g., a nonnull expression
does not have the value null at run time).
A qualifier validator
automatically ensures that a qualifier's rules respect the intended
invariant, for all possible C programs.
Project Members
Brian Chin
Shane Markstrum
Todd Millstein
Jens Palsberg
Publications
Inference of User-Defined Type Qualifiers and Qualifier Rules (ESOP 2006)
Brian Chin, Shane Markstrum,
Todd Millstein, and Jens Palsberg
Semantic Type Qualifiers (PLDI 2005)
Brian Chin, Shane Markstrum, and
Todd Millstein
Software
A binary release of the Clarity framework for user-defined type
qualifiers in C programs is available for x86/Linux here.
JavaCOP is a framework for user-defined type annotations in Java.
Programmers can employ annotations on Java classes, methods, fields,
and variables using Java 1.5's metadata facility. JavaCOP
enforces user-defined typing constraints for such annotations, which
are written in a declarative and
expressive rule language. In this way,
programmers are able to check that their programs will operate
correctly in restricted environments, adhere to strict programming
rules, avoid null pointer errors or scoped memory exceptions, and meet
style guidelines, while programming language researchers can easily
experiment with novel type systems. JavaCOP can therefore be
considered a framework for "pluggable type systems," whereby multiple
type systems can be easily be supported in the same language.
Project Members
Chris Andreae (Victoria University of Wellington, New Zealand)
Dan Marino (UCLA)
Shane Markstrum (UCLA)
Todd Millstein (UCLA)
James Noble (Victoria
University of Wellington, New Zealand)
Publications
A Framework for Implementing Pluggable Type Systems
(OOPSLA 2006)
Chris Andreae, James Noble, Shane Markstrum, and Todd Millstein
Software
The JavaCOP release is
here.