Additional operations on system states and their components.
These operations are used to formulate and prove the correctness of the system, along with the ones defined in operations. Unlike the latter, these operations are not used to define the state transitions of the system; this is why they are grouped separately.