[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.