Java Typestate Checker.

Detecting programming errors in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. Leveraging on the observation that in Object-Oriented Programming ( OOP ) it is natural to define stateful objects where the safe use of methods depends on their internal state, we present Java Typestate Checker ( JATYC ), a tool that verifies Java source code with respect to typestates. A typestate defines the object's states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object's protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses. To the best of our knowledge, this is the first OOP tool that simultaneously tackles all these aspects. • Java Typestate Checker is a tool that verifies Java code with respect to typestates. • It verifies that sequences of method calls obey to object's protocols. • It verifies that objects' protocols are completed. • It verifies that null-pointer exceptions are not raised. • It verifies that subclasses' instances respect the protocol of their superclasses.