State Inference for Dynamically Changing Interfaces

Types in current programming languages specify constant sets of messages always acceptable throughout the lifetime of the types' instances. However, especially in concurrent object-oriented systems, the acceptability of messages often changes with the objects' states. We propose a typed concurrent object calculus where static type checking ensures that users send only acceptable messages although message acceptability may change dynamically. The programmer specifies in types predictable state changes and dependences of message acceptance on states; a compiler infers the needed state information. This state inference has polynomial time complexity and can be used together with subtyping.