Operation ScopedName push (GenericName new), in Class ScopedName

Documentation
Push goes to the scope passed and finds its parent scope and creates a new ScopedName valid in the new scope where the head is the local name in the new scope for the current scope.



push().tail = self





push(S:Scope).head() = S


Protocol Qualification 
Exceptions Size 
Time ConcurrencySequential
Export ControlPublicAccess  


Preconditions


Postconditions


Semantics