• Given a state S, an operation O can be defined as $$O(args \times S) \rightarrow (R \times S’)$$, i.e. it returns a result R and updates the state to S’.
• However, Bertrand Meyer introduced Command-Query Separation in the 1980s, so you only need to know $$O(args \times S) \rightarrow (R \times S)$$ and $$O(args \times S) \rightarrow (\emptyset \times S’)$$.
• Various history “traces” can be considered equivalent and therefore a lot of knowledge about the historical state transitions elided, simplifying the reasoning. For example, given a well-designed stack, it is impossible to distinguish the history of stack.push(3); stack.pop(); stack.push(7) from stack.push(7).
• Various operations on the state are irrelevant to the behaviour of an operation under consideration. In reasoning about the final operation in a = 3; b = 7; c = 9; stack.push(2) you do not need to consider the assignment operations (and indeed their presence may indicate a cohesion problem in your design).
• The one remaining source of difficulty is aliasing; I do need to know about the elided operations in the sequence x = 7; *y = &x; ...; z=f(x). This is aliasing, not mutable state.