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 | | Concurrency | Sequential |
Export Control | PublicAccess | | |
Preconditions
Postconditions
Semantics