I like to think of it as "application-as-functional-specification".
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.
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.