Functional programmers like to claim that you can’t reason about mutable state programs. Some thoughts:
- the first half of the book A Discipline of Programming by Edsger W. Dijkstra tells you how to do it. That half of the book is approximately 100 pages (the remainder of the book is worked examples).
- object-oriented programming breaks a software system up into separate systems running miniature, message-driven programs as if on separate computers. Therefore the consideration of “mutable state” can be split in two: the state internal to the object and the state external to the object which sends messages to the object but is ignorant of its internals. If you can’t split the state that way, you have bad encapsulation.
- The reasoning done about the external and internal behaviours had better match at the interface. Design by contract probably helps here.
- 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 ofstack.push(3); stack.pop(); stack.push(7)fromstack.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.
