In this work we present the use of a novel language based on Gurevich Abstract State Machines[7] to specify active mobile objects semantics. We focus on the mobility
support based on the explicit interaction abstraction between units of specification. The mobility is expressed by changing the communication topology dynamically. The
interaction specification part of a unit also provides usual constructions, such as sequential, parallel, and non-deterministic composition, used to describe the synchronization
restrictions the units must preserve between themselves. We show how the proposed method provides a suitable way to reason about specifications.