  It is notoriously hard to correctly implement a multiparty protocol which
involves asynchronous/concurrent interactions and the constraints on states of
multiple participants. To assist developers in implementing such protocols, we
propose a novel specification language to specify interactions within multiple
object-oriented actors and the side-effects on heap memory of those actors; a
behavioral-type-based analysis is presented for type checking. Our
specification language formalizes a protocol as a global type, which describes
the procedure of asynchronous method calls, the usage of futures, and the heap
side-effects with a first-order logic. To characterize runs of instances of
types, we give a model-theoretic semantics for types and translate them into
logical constraints over traces. We prove protocol adherence: If a program is
well-typed w.r.t. a protocol, then every trace of the program adheres to the
protocol, i.e., every trace is a model for the formula of its type.
