TY - MANSCPT
TI - Computation and State Machines
AU - Lamport, Leslie
AB - I have long thought that computer science is about concepts, not languages. On a visit to the University of Lugano in 2006, the question arose of what that implied about how computer science should be taught. This is a first, tentative attempt at an answer.
DA - 2008/04//
PY - 2008
UR - https://www.microsoft.com/en-us/research/publication/computation-state-machines/
Second, the translation from a programming language to a state-machine formalization (i.e., with an initial state set and a next-state relation) is not only relatively simple, but the result is often very succinct and clear, as those who use TLA+ can testify. It is true that very few people, comparatively speaking, use mathematical formalization of any kind, but among those who do, the state-machine formalization is the most popular by a wide margin.
In such a model, state transitions can be as small or as large as you choose (e.g. sorting an array could be a single state change or multiple ones, depending on your chosen level of abstraction). Lamport's Temporal Logic of Actions (which forms the core, or at least the most interesting part of TLA+) has the very mathematical notion of abstraction as a first-class construct, i.e., A => B iff B is an abstraction of A (where => is the logical implication operator, which in TLA also means "refines" or "implements", i.e., the converse of abstraction).
What state is my radio in? When I receive this message what state does it move into? When I send this message what state does it move into? Etc.
Even if our programs aren't direct translations of this model, our specification comes out this way (or is better understood if you view it this way). All of our simulators take this model directly. Our automated testing, similarly, is done by using this state machine model of the system.