A basic calculus for verifying properties of interacting objects

摘要

We introduce a basic calculus for expressing and proving properties of interacting objects. The objects considered have dynamic behaviour and are organized into object communities in a hierarchical way. After a detailed and formal presentation of the calculus, essential properties of the calculus are discussed, especially the question of compositionality.The calculus 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. This calculus can be seen as an extensible basis applicable to different object-oriented specification frameworks.