D
D
Documentation
Search
⌃K

The ENFORCE statement

Purpose

The purpose of this statement is to automatically modify the population of a relation based on rules.

Syntax

Since ampersand 4.4.0 the syntax of this statement is:
ENFORCE <RelationRef> <type>?
<operator>
<Term>
The <operator> can be one of :=, :< or >: .
This statement may occur anywhere within a context, either inside or outside a pattern.

Semantics

This statement means the population of the relation will automatically be kept respectively equal ( :=), a subset (:<) or a superset (>:) of the population of the given term.

Examples

ENFORCE r := s;t
{- Ampersand will keep the population of the relation r equal to the population
of the expression s;t . It will do so by changing the contents of r
without affecting the contents of s;t .
The effect can be observed in the prototype.
-}
ENFORCE canDrive :< hasCar /\ hasDriverLicence
{- Ampersand will keep the population of the relation canDrive smaller than
the population of the expression hasCar /\ hasDriverLicence .
It will do so by deleting pairs from the contents of canDrive
without affecting the contents of hasCar /\ hasDriverLicence .
So, whenever a person can drive, that person needs to have a car and a driver licence.
However, if that person has both these assets, it is still possible that he/she
cannot drive.
-}

Miscellaneous

  • Both the sources and the targets of the relation and the term must match. An error message is given otherwise.
  • The relation must be specified in order to use it here, as is the case with any relation used in an expression.