Java Annotations for Invariant Specification
Where: Rice University Computer Science Department, RAP Seminar
When: September 22, 2008
Java annotations allow programmers to attach metadata to programs. During normal execution, the annotations are ignored, but in contrast to comments in the source code, annotations can be manipulated programmatically at compile- or run-time.
In this talk, I provide a brief introduction to Java annotations and show how limited their use currently is. I then describe a framework for specifying program invariants using Java annotations, and how extending Java to support subtyping for annotations allows programmers to write the invariants in a succinct manner.
