Treffer: Open Effects: A Hybrid Type-and-Effect System to Tackle Open World Assumption and its Application to Optimistic Concurrency
Weitere Informationen
This work tackles the challenge of applying a type-and-effect system to reason about object-oriented programs with an open world assumption. An open world assumption chal-lenges the design of a type-and-effect system when (1) all subclasses of a class are not known, and (2) an upper bound on effects of all subclasses is not available, e.g. when an ef-fect specification is not available for that class – a common phenomenon in modern OO programs. The main problem is in the computation of the effects of a dynamically dispatched method invocation, because all possible dynamic types of its receiver are not known statically, and no static upper bound in the form of effect specification is available. Our new con-cept open effects solves these problems. The basic idea is to take a programmer-guided hybrid approach. Instead of using