Simple StackADT Component

component StackADT is
    interface
        top_domain
            in
                null;
            out
                null;
        bottom_domain
            in
                PushElement (value : stack_type);
                PopElement ();
                GetTopElement (); 
            out
                ElementPushed (value : stack_type);
                ElementPopped (value : stack_type);
                TopStackElement (value : stack_type);
                StackEmpty ();
    parameters
            null;
    methods
            procedure Push (value : stack_type);
            function Pop () return stack_type;
            function Top () return stack_type;
            function IsEmpty () return boolean;
    behavior
        received_messages PushElement;
            invoke_methods Push;
            always_generate ElementPushed;   
        received_messages PopElement;
            invoke_methods IsEmpty, Pop;
            always_generate StackEmpty xor ElementPopped;   
        received_messages GetTopElement;
            invoke_methods IsEmpty, Top;
            always_generate StackEmpty xor TopStackElement;   
    context
        top_most ADT
end StackADT;