Bica is an extension of the Java language that enables the verification of Java programs against a session type specification.
This specification represents the changes in the interface of an object.
In Java, the interface of an object is the set of methods declared in the object’s class, with visibility taken into account.
Session type specifications provide a more flexible way to specify changes in the interface of an object.
The session type is included in the source code for a class as a Java annotation.
Types are extended with session type information, and Bica verifies that clients of a class use it as specified by the session type.
Bica is implemented using the Polyglot framework, as an extension of the jl5 language extension. That is, it supports Java 5 source code.
