39 Constraint Forms

Predica supports several forms of constraints, each governing different aspects of the values and relationships in a model.

• Attribute type constraints:
  These restrict the possible values of an attribute.

  
          X x;            // Each value of x must be of type X
          

• Attribute cardinality constraints:
  These constrain the cardinality of an attribute's extension.

  
          X x[1..3];      // Cardinality of extension of x must be between 1 and 3
          

• Key constraints:
  Keys identify when two instances of a nominal type represent the same entity.

  
          entity X
          {
              Name name;
              Integer value;
              key { name };       // Instances of X with the same name are the same
          }
          

• Derived attribute constraints:
  A derived attribute is constrained by the expression that defines it.

  
          value Rectangle
          {
              Real width;
              Real height;
              → Real area = width*height;       // constrained by expression
          }
          

• Where‑constraints on attributes:
  A where‑clause restricts the value of an attribute.

  
          entity Supplier
          {
              String name;
              Shipment shipment* 
                  where shipment.supplier = this;   // where constraint on shipment
              key {name};
          }
          

• Constraint blocks:
  A nominal type may include a constraints block containing Boolean expressions, each terminated with ;.

  
          entity Person
          {
              String name;
              Boolean registered_to_vote;
              Integer age;
  
              constraints
              {
                  ¬name.empty();
                  registered_to_vote → age ≥ 18;
              }
          }
          

Constraint expressions

A constraint expression may appear in a where clause or a constraints block.

A constraint expression must be Boolean-valued. It may use:

• logical connectives ¬, ∧, ∨ and →
• Parentheses
• Truth constants: true and false
• Boolean-valued path expressions (including sentences such as path.())
• Comparison operations <, ≤, >, ≥, = and ≠.

Predica uses a single expression grammar for both path expressions and logic expressions. This allows a single expression to freely mix logic connectives (¬ ∧ ∨ →) with path constructs (. ⇒ ⊓ ⊔ | \ [] () ! ~). The result is interpreted as a logical formula parameterised by the terms introduced by path expressions. The overall expression may itself be a path expression, allowing shared path prefixes and compositional navigation.

For example:

entity A
{
    Boolean x;
    Boolean y;
}

entity B
{
    A z*;
    constraints
    {
        // ∀Z:A ∀X:Boolean ∀Y:Boolean (this.z(Z) ∧ Z.x(X) ∧ Z.y(Y)) → (X ∨ Y)
        z.(x ∨ y);
    }
}

Cardinality constraints in path expressions

Predica allows : for writing cardinality constraints on path expressions. In the following example b:2 expresses the condition that the cardinality of the extension of b is exactly 2:

entity X
{
    Boolean a;
    Integer b*;
    constraints
    {
        // Shorthand for a → b.Σcount=2
        // ∀A:Boolean this.a(A) → (A → |{B:Integer|this.b(B)}| = 2)
        a → b:2;
    }
}

A cardinality constraint on a path expression uses the syntax:

path : k        // exactly k
path : k..m     // between k and m inclusive
path : ?        // 0 or 1
path : +        // 1 or more
path : k+       // k or more

where k and m are integer literals.

Cardinality binds looser than path composition, so it constrains the complete path expression to its left. For example, licence.[valid]:1 is parsed as (licence.[valid]):1, not as licence.([valid]:1).

This syntax mirrors attribute cardinality (x?, x+, x[k], x[k..m]).