To tackle the challenge of finding bugs in object-oriented code, where objects naturally have protocols, following previous work on associating behavioural types with object-oriented languages, we have been developing JaTyC, a typestate-based checking approach for Java. The recipe is simple: attach protocols (essentially, allowed orders of method calls) to classes and type check classes (i.e., their method bodies) following the protocol, thus gaining typestate-based nullness checking (ensuring memory-safety), protocol compliance, and protocol completion (under program termination).

Existing approaches, like Mungo, provide very limited support for inheritance and polymorphism. Our initial solution exploited the seminal simulation-based notion of subtyping to check that the protocol of a class is a subtype of the protocol of its superclass. However, we only allowed upcast and downcast at the beginning of an object’s protocol (i.e., just after object creation) or at the end (i.e., in the end state). Additionally, to determine if a typestate is a subtype of another, the algorithm was only applied to the initial typestates of the protocols. It is fundamental to overcome these limitations to make the typestate approach applicable to real-world scenarios.

Our solution is language agnostic and applicable to many object-oriented languages. We developed and mechanised the casting theory, provably showing it is sound. To test its expressiveness, we extend JaTyC to now support casting in the middle of a class protocol.