Constraints are useful for stating succinctly when things do not change in value. Consider the following MaxCounter machine whose state variable x can never exceed the value of the other state variable max. Max is initialized to 15 and its value never changes.
MaxCounter = (
=
1
incĒ(i: int) pre
post
It's trivial to show the following constraint:
This kind of example may look simplistic but it generalizes to any system where you want to ensure that some state variable never changes. When we have a huge state space (as is more typical of software systems than in my zillions of simple counter examples), very often we are careful to state how some state variable changes but forget to say what state variables do not change. Constraints are a nice way to describe those properties.