We propose a type system for _object usage analysis_ in Java bytecode
(JVML), which verifies the order in which methods of each object are
invoked.

It is desirable from the viewpoint of both debugging and security that
objects in a program are used in valid manners, i.e., according to the
intention of the programmer or the library provider.  For example, we
expect that a File object is first created and initialized, then
opened before read or written, and finally closed (and no more used
after that).  The current verifier of JVML, however, does not check
such validity of object usage.

To improve this situation, we construct a type system for analyzing
object usage in JVML, adopting three key ideas from Kobayashi et al.'s
generic type system for pi-calculus, object locking analysis for JVML,
and resource usage analysis for lambda-calculus.  The first key idea
is to extend the type of an object with its _usage_, information about
how the object is going to be used (specifically, the order in which
methods of the object are invoked).  The second is to extend type
environments so that they keep track of the usage information even
across different variables, in order to deal with aliases.  The third
is to treat write and read operations on object fields (putfield and
getfield) as usage of the object, in order to handle destructive
updates.