Why Alloy has no in-built Notion of State

A few years ago Daniel Jackson took the rather surprising step of actually removing in-built support for states from the Alloy specification language. Here he explains why:

the main advantage of the old scheme was that, with the notion of pre and post built in, certain mutability constraints could be built in too. when you declared a state component, you could say how it changed.

but it turns out that priming as an operator is much more complicated than you would imagine. it made for all kinds of kludges in the implementation, which was a sure sign that the semantics was too complicated. and sure enough, if you take a look at the semantics of sequential composition in the Z standard, you'll see that it's full of subtle details and is really quite ad hoc.

the main reason we dropped it, tho, was that we wanted to be able to handle dynamic behaviour with more flexible idioms. with that priming convention, you're really tied to a rather narrow way of writing models. having got rid of it, we can do more ambitious things -- talking about sequences of more than a pair of states, for example.

(From the alloy-discuss group.)

One of the reasons that I became disillusioned with Z and its object-oriented extensions was that they had become bogged down in a state-based view of specification. This seemed to me to be so limiting. It was as if the developers of Z were satisfied with just aping programs. They didn't seem to be interested in going any further. I wanted more, and I am glad to see that Daniel Jackson does too.