A Type Safe State Abstraction For Coordination In Java-like Languages

摘要

this feature.We develop a type and effect system, which guarantees that, during execution of a method invoked on a concurrent object o: (1) No attempt will be made to access fields not available in the current state of o, and (2) No method invoked on a receiver (syntactically) different from this may cause the invocation of a method on o. The latter guarantee helps to enforce the former and prevents a family of accidental violations of the intended coordination protocol.