(*
        Definition of the quality attribute - Object-orientedness
        An object-oriented program uses classes to model its user-domains
        entities or events.
*)

object Entity;
object Event;
object UserDomainEntity =  Entity*;
object UserDomainEvent =  Event*;

operation IsUserDomainEntityClass(Entity)-> (boolean);
operation IsUserDomainEventClass(Event) -> (boolean);


operation ProgramIsOO
        inputs: d1: UserDomainEntity, d2: UserDomainEvent;
        outputs: boolean;
        pre:     ;
   post:    
                forall (t in d1) IsUserDomainEntityClass(t)
                and
                forall (t in d2) IsUserDomainEventClass(t);
end ProgramIsOO;