[P1] _________________________ AMAST Links 01 02

Algebraic specification of object-orientedly modeled data types

Erik Wilde (wilde@tik.ethz.ch)

I got the address of this mailing list from a colleague who proposed to ask you about my problem. Since I'm not a member of this list, please send answers directly to me and not to the list. I shall collect the replies and make them available through an announcement to this list. Thanks. And here's my problem, which is concerned with the algebraic specification of OO modeled data tys. I have three classes of objects
  1. An Entity is every object represented within my universe
  2. A User is a subclass of Entity (ie every User is an Entity) and represents users within my universe
  3. A Group also is a subclass of entity (ie every Group is an Entity) and represents groups of entities (ie users or groups) within my universe

The idea is that class Entity will never be instantiated (an abstract base class in C++ terminology), but is used to specify all properties common to User and Group. Now there are operations defined on these classes, eg

join: entity, group -> group
leave: entity, group -> group
which are used to assign or delete entities (ie users or groups) to resp. from groups. There are other operations which operate on entities and I also need operations which operate on all entities (eg search for a user with a specific name). As far as I understand, ACT ONE does not support inheritance. If this is correct, could some of you give me a hint which formalism would be appropriate to specify (and maybe verify) my approach? I also need some constraints, eg for each group there may be a maximal number of members (members can be users or groups), and the operation join should only add an entity to the group if this number is not yet reached. Another example of constraint is as follows. Each group has a flag which can restrict membership to users (this way it would be possible to prohibit nested groups). Consequently, the operation join should fail, if this flag is set and it is tried to add a group to the group. As you can see, object orientation is important for my model. I would be really thankful for any hint or pointer to appropriate literature.