does not occur, it is very possible that a user will iterate "off the end of" a Collection. The figure to the right shows a finite state machine that defines a possible monitor for checking and enforcing this property with runtime verification. From the "unknown" state, it is always an error to call the codice_3 method because such an operation could be unsafe. If codice_2 is called and returns true, it is safe to call codice_3, so the monitor enters the "more" state. If, however, the codice_2 method returns false, there are no more elements, and the monitor enters the "none" state. In the "more" and "none" states, calling the codice_2 method provides no new information. It is safe to call the codice_3 method from the "more" state, but it becomes unknown if more elements exist, so the monitor reenters the initial "unknown" state. Finally, calling the codice_3 method from the "none" state results in entering the "error" state. What follows is a representation of this property using parametric past time linear temporal logic.