An Exception Aware Behavioral Type System for Object-Oriented Programs

We develop a type system for object oriented languages that combines standard type information with behavioral protocol specifications. The typing rules cover familiar constructs, as well as exceptions, which are a main novelty in this work: exceptions may cause abrupt control transfer in allowed behaviors, and have been particularly difficult to tackle with behavioral type systems. The type system guarantees protocol fidelity both at the method level and at the class level by checking consistency in the use of fields with the class’ usage protocol. It also ensures that program execution always reaches a safe termination state, even in the presence of behavioral borrowing, that is, temporary aliasing of object references during methods calls.