A functional specification for a stateful system is a function from a list of all inputs to an output, i.e. `fun spec(inputs: List(Input)): Output`.
This kind of specification doesn't need to specify `State` at all, as we can simply refer to previous inputs. E.g. imagine a counter system with the inputs `Increment`, `Reset`, and `Get`. The functional spec for `Get` is "find the latest reset and then count the number of `Increment`s since then".
I think this is neat, because if you are developing the functional spec with a domain expert that doesn't know programming you don't wanna bother them with, for them, unnecessary bookkeeping details.
From this spec you can then figure out what `State` needs to be, but this can be done as a separate step not involving the domain expert but rather other developers.
I learnt this from the Cleanroom software engineering people, they call the spec without `State` a "black box spec", while the one with `State` is called a "state box spec". (There's also a third step called "clear box spec" where they break down the "state box spec" into functions.)
I've been playing around with the idea of designing a specification language that lets you write "black box specs" together with some basic sanity checks of those specs, because I think there's a lot of value in this sort of structure.
For example even if your application doesn't follow the "application-as-function" pattern, you can still use your "state box spec" as an oracle when doing property-based testing of your application.