> That was the second part of my answer: a graph on paper. Draw nodes of execution and represent the branch as two arrows coming from the node and heading to new nodes. Label the arrows with the predicates of the branch.

Thanks! You don't happen to have some learning resources for modelling programs as state machines? I can't find anything when I search.

This is more of a practical writeup on state machines than a theoretical one: http://gameprogrammingpatterns.com/state.html

You might also know these as flowcharts when applied to program flow control.

I don't think I answered the original question well. I just wanted to point out that math is more than just equations. Others have done a much better job in this thread.

This isn't about modelling rather a programming technique, but check out Idris for its dependent typing. It lets you encode state machines in types, which means your programs literally will not typecheck if you try for example to withdraw money from an unauthorized ATM, or candy from an empty store. You can make verified network protocols and drivers like this.