Technical Report Number
The open world assumption in modern object-oriented languages makes the design of a type-and-effect system challenging. The main problem is with the computation of the effects of a dynamically dispatched method call, because all possible dynamic types are not known in advance. We show that the open world assumption and the need for a type-and-effect system can be reconciled. We propose open effects, an optimistic effect assumed to satisfy the effect-based property of interest. We describe a sound type-and-effect system with open effects which has two parts: a static part that takes effects of dynamically dispatched calls with certain special references as open effects; and a dynamic part that manages dynamic effects as these special references change and verifies that the optimistic assumptions about open effects hold. This system is implemented in the Open-JDK compiler, and its utility is tested by applying it to verify noninterference of concurrent tasks.