67 Constraints

A constraint is part of a nominal type. It is an axiom that restricts the values belonging to that type. The transaction-boundary application and enforcement rules are specified in Constraint-Violating Updates.

Constraints are written in a constraints block. Stored attribute declarations also provide a where shorthand, described below.

Every constraint expression must have type Boolean.

Supported nominal types

A constraints block may be used in value type, entity type, variant type, and quotient type declarations. It may not be used in an enum declaration. An enum defines a fixed set of attributes; restricting that set should instead be expressed by declaring the intended enum or an appropriate enum subtype.

Stored-attribute `where` clauses

A where clause following a stored typed-attribute declaration is syntactic sugar for adding its expression to the constraints block of the enclosing nominal type. For example:

value Point
{
    Real x where x > 0;
    Real y;

    constraints
    {
        x < y;
    }
}

is equivalent to:

value Point
{
    Real x;
    Real y;

    constraints
    {
        x > 0;
        x < y;
    }
}

The where expression is evaluated in the same receiver context as an expression written directly in the type's constraints block. It may therefore refer to other attributes of the enclosing type; its placement after one attribute does not give it a narrower scope or make it a property of that attribute's payload type.

Several constraints may follow one attribute by separating their expressions with commas. Each expression becomes a separate constraint on the enclosing type:

Real percentage where percentage ≥ 0, percentage ≤ 100;

The where shorthand is not permitted on a derived attribute or an embed declaration. A constraint involving either must be written explicitly in the enclosing constraints block. This keeps where narrowly associated with the validity of stored attribute values and avoids making a derived definition look as though it carries a local result postcondition.

Constraints on derived attributes

A constraint may refer to derived attributes as well as stored attributes. The derived expression is evaluated according to its definition, and the resulting value participates in the constraint like any other attribute value. For example:

value Rectangle
{
    Real width where width ≥ 0;
    Real height where height ≥ 0;
    → Real area = width * height;

    constraints
    {
        area ≤ 100;
    }
}

Here area is derived rather than stored, but it may still be named by the constraint. The constraint restricts Rectangle values to those whose derived area is at most 100. This does not cause area to be stored or independently assignable. Such a condition must be placed in the explicit constraints block; it cannot be attached to the derived declaration with where.

Effect on carrier sets

Constraints refine carrier sets. If a type body has unconstrained structural carrier carrier(S) and constraints K, then the constrained carrier is:

carrier(S with K) =
{
    v ∈ carrier(S)
    |
    K(v)
}

Constraint expressions are interpreted over attribute extensions. For example:

value P
{
    Real x*;
    Real y*;

    constraints
    {
        x < y;
    }
}

has values of the form:

((x, X), (y, Y))

where X ⊆ Real, Y ⊆ Real, and:

∀x ∈ X. ∀y ∈ Y. x < y

Geometrically, the derived locus of such a value is X × Y in the (x,y) plane, and the constraint requires the whole product locus to lie in the open half-plane x < y. Arbitrary subsets of that half-plane, such as curves or disks, are not values of this type merely because their points satisfy x < y. Correlated point sets are represented by repeating a structured point value, for example:

value Point
{
    Real x;
    Real y;

    constraints
    {
        x < y;
    }
}

value Q
{
    Point p*;
}

In Q, the extension of p is a set of Point values. Each repeated Point carries its own correlated x and y extensions.

Disjoint declarations

Experimental: a constraint-level disjoint declaration is a possible shorthand for stating that several attribute paths have pairwise disjoint extensions. No decision has yet been made about whether this special syntax will remain part of Predica, and implementations are not currently required to support it.

For example, an assignment could require that no person occurs as both a supplier and a customer:

entity Assignment
{
    Person supplier*;
    Person customer*;

    constraints
    {
        disjoint { supplier, customer };
    }
}

This declaration can be regarded as syntactic sugar for an ordinary empty-intersection constraint:

supplier ∩ customer = ∅;

With more than two paths, the declaration means that every pair has an empty intersection. Thus:

disjoint { supplier, customer, reviewer };

is shorthand for:

supplier ∩ customer = ∅;
supplier ∩ reviewer = ∅;
customer ∩ reviewer = ∅;

This path-level constraint is distinct from a top-level type disjointness declaration such as disjoint Supplier, Customer;. The latter records a fact about the carrier sets of types; the experimental constraint form compares the extensions obtained from paths in the current receiver context. Until the special form is adopted, programs can express the same property with the ordinary expression constraints shown above.

Inclusion dependencies

The Supplier-and-parts database provides an example of how inclusion dependency constraints are written in Predica:


entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
    constraints 
    {
        shipment.supplier.Σ ⊆ supplier.Σ;
        shipment.part.Σ ⊆ part.Σ;
    }
}

This relies on path expression syntax for writing queries, discussed in Part VII: Query. The .Σ fold collects path values into sets so they can be compared by inclusion. For example, the constraint shipment.supplier.Σ ⊆ supplier.Σ says the suppliers of shipments must be a subset of the suppliers.

This formulation works directly at the level of domain objects, independently of the choice of keys. It continues to work unchanged even when keys are composite.

Predica’s key-independent formulation of inclusion dependencies contrasts with SQL, where referential integrity constraints are expressed in terms of foreign keys.

Previous66 Ordering Next68 Theorems