Example: necessary and single

The following metaformula ensures the necessary property of attributes, which are instances of the category Class!necessary. The semantics of this property is, that for every instance of the source class of this attribute there must exist an instantiation of this attribute.

Class with constraint, attribute
        necConstraint:
        $ forall p/Class!necessary c,d/Class x,m/VAR 
                 P(p,c,m,d) and In(x,c) ==> 
                 exists y/VAR  In(y,d) and A(x,m,y) $
end

It reads as follows:

For each attribute-link with label m between the classes c and d, which instantiates Class!necessary and for each instance x of c there should exist an instance y of d which is destination of an attribute of x with category m.

One should notice that the literals In(x,c) and In(y,d) cause this formula to be a metaformula. The instantiation of x and m to the class VAR is just a syntactical construct. Every variable in a constraint has to be bound to a class. This restriction is somehow contrary to the concept of metaformulas and the VAR-construct is a kind of compromise. The resulting In-literals are discarded during the processing of metaformulas. The VAR-construct is only allowed in metaformulas. It enables the user to leave the concrete classes of x and m open, without instantiating them to for example to Proposition.

The single-constraint can be defined in analogy. These constraints can be added to the system as if they were ``normal'' constraints. Their effect becomes visible, when declaring attributes as necessary or single. This is done in the following model.

{**************************}
{*                        *}
{ File: ERSingNec         *}
{*                        *}
{**************************}

{* necessary constraint (metaformula) *}
Class with constraint, attribute
    necConstraint:
    $ forall p/Class!necessary c,d/Class x,m/VAR 
      P(p,c,m,d) and In(x,c) ==> 
         exists y/VAR  In(y,d) and A(x,m,y) $
end 




{* every Entity has a key *}
Class EntityType with
  attribute, necessary
     keyeAttr : Domain
end 


{* single constraint (metaformula) *}
Class with constraint, attribute 
singleConstraint : 
   $ forall p/Class!single c,d/Class x,m/ VAR 
     In(p,Class!single) and P(p,c,m,d) and In(x,c)  ==> 
        forall y1,y2/VAR 
        In(y1,d) and In(y2,d) and A(x,m,y1) and A(x,m,y2) ==>  
                 IDENTICAL(y1, y2) $
end

{* every Entity key is monovalued ( = necessary and single)*}
Class EntityType with rule
     keys_are_necessary:
        $forall a/EntityType!keyeAttr In(a,Class!necessary)$;
     keys_are_single:
        $forall a/EntityType!keyeAttr In(a,Class!single)$
end

The effects of this transaction can be shown by displaying the instances of instances of the class metaMSFOLconstraint. The single- and necessary constraints are inserted into this class after adding them to the system. These constraints themselves can have instances: constraints which are added automatically to the system when inserting objects into the attribute-category single resp. necessary.

For the ER-example, one of the created formulas reads as:

$ forall x/EntityType   
  In(EntityType,Class) and In(Domain,Class) ==> 
    (exists y/Domain   A(x,eAttr,y) and (TRUE)) $

This formula contains redundant literals which are not optimized in our current release. Observe the relationship to the necessary-formula: The formula has been generated by computing one extension of In(p,Class!necessary) and P(p,c,m,d) and replacing the literals In(p,Class!necessary and P(p,c,m,d) by this extension, which results in the following substitution for the remaining formula: