Declarative vs. Operational (Imperative) Modeling

Roughly speaking, there are two ways to describe a system: operationally (also called "imperative") and declaratively. An operational modeller asks "how would I make X happen?". A declarative modeller asks "how would I recognize that X has happened?". In many contexts, it is more natural and concise to use a declarative description. Often one need only to describe the rules of the game and what it means to have won, and not even think about what moves will be needed (and which must be avoided) in order to win.

In the spirit of being declarative, the order of statements in an Alloy model does not affect its meaning (as long as they remain syntactically well-formed). All the constraints must hold, but there is no notion of an ordering on them.