Cornell Department of Computer Science Colloquium
4:15pm, Friday November 9th, 2001
B17 Upson Hall

Lightweight Specifications Through Type Qualifiers

Alexander Aiken
UC Berkeley

There are many useful properties of programs that could be inferred or verified easily if only programmers annotated their software with specifications. But programmers seem to resist writing specifications, to put it politely. In trying to answer the question, "What specifications will programmers write?" we have been led to a small extension of standard type systems that allows programmers to define and use their own type qualifiers. Just as type qualifiers such as "const" and "volatile" extend C's types with properties that are otherwise not expressible, user-defined type qualifiers give programmers a simple way to define, express, and check important system invariants.