Syntax for pred (predicate) statements

pred name [parameter1:domain1, parameter2:domain2] {
     constraint1
     constraint2
     constraint3
}

If the inputs satisfy all of the constraints listed in the body, then the predicate evaluates to true. Otherwise it evaluates to false.

In an imperative model, you might ask yourself "how can I make X happen?". In a declarative model (like Alloy), you ask yourself "how would I recognize that X has been accomplished?".

One reflection of this is that predicates in Alloy only ever evaluate to true or false, while function may evaluate to relations.

A predicate returns true or false. A similar construct is a function which returns a value.

Remind me what a function is.