The basic rules suffice for many purposes (e.g., for describing the C programming language [GH]), but they do not suffice to model all sequential algorithms. A sequential algorithm may add a new node to a graph or create a new message. We need rules that allow us to create new nodes, new messages, etc., and such rules are introduced in this subsection. However, we do not create new elements; instead, we use a special universe Reserve from which the new elements come.
In this section we use individual variables, but only in a limited way. (Variables are used more extensively in .) Roughly speaking, only bound variables are used; free variables appear only in contexts where some values have been assigned to them.