Java Annotations For Invariant Specification

Java Annotations for Invariant Specification RICE UNIVERSITY

COMPUTER SCIENCE

Mathias Ricken September 22, 2008 COMP 617 Seminar

2

Comments are dumb class HashMap { // returns null if no mapping for key Object get(Object key) { … } } HashMap m = new HashMap(); Object o = m.get("foo"); String s = o.toString(); NullPointerException at runtime: o is null

3

Types are smart class HashMap { // returns null if no mapping for key Object|null get(Object key) { … } } Compiler Error: Return type Object|null incompatible with type HashMap m = new HashMap(); Object Object o = m.get("foo"); String s = o.toString();

This is not Java!

4

Annotations can make Java smarter class HashMap { // returns null if no mapping for key @Nullable Object get(Object key) { … } } HashMap m = new HashMap();

Compiler Warning: Return value may be null, assigned to non-null variable.

Object o = m.get("foo"); String s = o.toString();

Pluggable type systems in Java 5 7?

5

Annotation Targets in Java 5 @A package some.package.name; @B class MyClass { @NonNull Object field; @C MyClass(@NonNull Object param) { field = param; } @NonNull Object method() { @NonNull Object localVar = field; return localVar; } } Note: Local variable annotations are completely ignored.

6

Concurrency Invariants interface TableModel { // may only be called from event thread void setValueAt(…); }

TableModel m; // from outside event thread… m.setValueAt(…);

Possible race condition.

7

Invariant Specification interface TableModel { @OnlyEventThread void setValueAt(…); }

TableModel m; // from outside event thread… m.setValueAt(…);

Invariant Violation Warning at Runtime (but still possible race condition)

8

Comparison to assert void setValueAt(…) { assert (EventQueue.isDispatchThread()); …

Similarity  Debug mode – disabled in production code

@OnlyEventThread void setValueAt(…) { … }

9

Annotations are Easier to Find

 Javadoc

produces invariant index

10

Inherited Invariants TableModel Object getValueAt(…) @OnlyEventThread void setValueAt(…)

Implied @OnlyEventThread

AbstractTableModel Object getValueAt(…) void setValueAt(…)

DefaultTableModel Object getValueAt(…) void setValueAt(…) Implied @OnlyEventThread

MySpecialTableModel Object getValueAt(…) void setValueAt(…) Implied @OnlyEventThread

11

Inherited Invariants @OnlyEventThread TableModel Object getValueAt(…) void setValueAt(…) Implied @OnlyEventThread

AbstractTableModel Object getValueAt(…) void setValueAt(…)

DefaultTableModel Object getValueAt(…) void setValueAt(…) Implied @OnlyEventThread

Implied @OnlyEventThread

MySpecialTableModel Object getValueAt(…) void setValueAt(…) Implied @OnlyEventThread

12

Limited Universality A

few supplied invariant annotations

@OnlyEventThread @OnlyThreadWithName @OnlySynchronizedThis

 assert

@NotEventThread @NotThreadWithName @NotSynchronizedThis

can test an arbitrary predicate

assert (someComplexPredicate());

13

Predicate Invariant Annotations @PredicateLink(value=Predicates.class, method="eval") public @interface OnlyThreadWithName { String value; hod t e } em t a dic e r dp n i 1. F @OnlyThreadWithName("main") void myMethod() { … } Return true or false to indicate violation

3.

2. Call predicate method and pass as arguments: • this (nor null if static) • data in invariant annotation

public class Predicates { public static boolean eval(Object this0, String name) { return Thread.currentThread().getName(). equals(name); } }

14

Further Limitation of Annotations 

One occurrence of an annotation class per target @OnlyThreadWithName("main") // illegal; and is @OnlyThreadWithName("other") // this "and" or "or"? void myMethod() { … }



Suggestion @Or({ @OnlyThreadWithName("main"), @OnlyThreadWithName("other") }) void myMethod() { … }

15

Annotation Members

extends OtherAnnotation not allowed  no subtyping

@interface MyAnnotation { int String Class SomeEnum

intMember; stringMember; classMember; enumMember;

// // // //

primitives strings class literals enums

// annotions OnlyThreadWithName annotMember; // arrays of the above OnlyThreadWithName[] arrayMember; }

16

No Annotation Subtyping in Java @interface Or { OnlyThreadWithName[] value; }

@Or({@OnlyThreadWithName("main"), @OnlyThreadWithName("other")}) void myMethod() { … } // legal

@Or({@OnlyThreadWithName("main"), @NotThreadWithName("other")}) void otherMethod() { … } // illegal

No

common supertype for annotations

17

xajavac Modified Compiler @interface Base {} @interface OnlyThreadWithName extends Base { String value; } @interface NotThreadWithName extends Base { String value; } @interface Or extends Base { Base[] value; }

18

Results 

Annotations with Subtyping  Minimal

changes to the compiler  No changes to class file format  Reduced invariant checker by ~1500 lines  Improved code reuse

19

Results 

Invariant Annotations  Annotated

part of Swing and DrJava  Discovered and fixed some bugs in DrJava  Hard to do retroactively and without inside knowledge

20

Future Work 

Reflection library for annotations with subtyping  Annotation

getAnnotation(Class c)

currently returns the annotation of class c  Annotation[]

getAnnotations(Class c)

should be added to return all annotations of class c and its subclasses 

Modify JSR 308 prototype compiler to support subtyping

21

More Information and Download 

Invariant Specification  http://www.concutest.org/tc/



Annotations with Subtyping  http://www.cs.rice.edu/~mgricken/research/xajavac/