The global annotation declares global variables that can be analyzed along with the procedure parameters. These annotations simply provide a list of names that can be used to track global state information, and are not associated with a specific procedure. Like the on_entry and on_exit annotations, they need not correspond to actual global variables in the implementation. It is often useful to define global variables that model system states not explicitly represented by variables in the program. As examples, a global variable annotation can be used to track whether a library is properly initialized, or to maintain a record of outstanding asynchronous operations.