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.