We introduce a basic calculus for expressing and proving properties of synchronously interacting objects. The objects considered have dynamic behavior and are organized into object communities in a hierarchical way. We present syntax and semantics of the calculus in detail. Moreover, a set of basic inference rules is given. Essential properties of the calculus are discussed, especially the question of compositionality. The calculus developed constitutes a basis for investigating issues of verifying properties of objects and object communities. In consequence, we have focused on a small number of essential concepts. We hope that this calculus can contribute to gain experience in verifying objects. Therefore, a prototype implementation of the calculus using a generic theorem prover has been developed.