Quantification

In addition to primitive functions and operators, the Acme predicate language provides a limited quantification mechanism.  Both universal and existential quantification are supported, with the limitation that all quantification must be done over finite sets.  This limitation insures that the satisfaction of any predicate expression is computationally decidable.  Although limiting quantification to finite sets reduces the range of expressions that can be specified in the predicate language, the guarantee of computational decidability more than offsets this limitation. Further, a sufficient range (and possibly the bulk) of the predicate expressions of interest to software architects and environment designers can be expressed using quantification over finite sets.

Quantified predicates use the following syntax in the predicate language. 

QuantifiedPredicate ::=  ( forall | exists ) Identifier ( , Identifier)* : TypeExpression
                           in SetExpression  ( , Identifier ( , Identifier)*
                           : TypeExpression in SetExpression )* 
                                   
| PredicateExpression ;

 

Quantified predicates are boolean functions that evaluate a predicate expression for all members of a finite set of values. The keyword forall indicates a universal quantification and the keyword exists indicates an existential quantification.  The following examples illustrate the use of simple quantified predicates.

Forall comp : aCompType in sys.Components | comp.secure = True;    

Exists conn : connector  in sys.Connectors |DeclaresType (conn, EventSystemType);

 

Quantified predicates may be embedded within other quantified predicates.  For example:

Forall comp : aCompType in sys.Components |

                  Forall port : aPortType in comp.Ports | port.protocol = RPC;           

Forall comp : aCompType in sys.Components |
                      
Exists conn : aConnType in sys.Connectors |

                           Connected(comp,conn);

 

As the syntax specification indicates, quantified predicates are not limited to single variables.  Multi-variable quantifications are supported.  The following predicate is true in systems where all components are connected to all other components by at least one connector, forming a fully connected graph.  Admittedly, this example probably better illustrates complex quantifications than clean system design.

Forall c1, c2 : component in sys.Components |
          
Exists conn : connector in sys.Connectors |

                  Attached (c1, conn) and Attached (c2, conn)

 

 

 

Set expressions and set constructors

As mentioned earlier in this section, variables can only be quantified over finite sets.  The Acme predicate language provides a number of set operators and constructors for creating an appropriate set for quantification.  The syntax for the SetExpression nonterninal used in the syntax production of QuantifiedPredicate follows:

SetExpression     ::= SetLiteral  | Identifier  | SetFunction | SetConstructor

 

SetLiteral             ::= { } |  { (Literal | Identifier) (,Literal | , Identifier )* }

 

SetFunction                  ::= Primitive-Function ( ActualParams )
                          
| DesignAnalysisIdentifier ( ActualParams )
 

SetConstructor    ::= { select variable in SetExpression | PredicateExpression }
     
| { collect variable.substructure in SetExpression | PredicateExpression }

              

The standard ways for specifying and/or creating a set over which a variable will be quantified include (1) explicitly specifying a literal set, (2) referring to an existing set, (3) calling a function that returns a set type, or (4) constructing a set using the select or collect set constructor operators.  The following examples illustrate each of these four methods.

(1)        Forall x : int in { 1, 2, 3, 4, 5 } | P(x)

(2)        Forall x : port in self.ports | P(x)

(3)        Exists x : port in union(foo.ports, bar.ports) | P(x)

(4)        Forall x : component in
         { select c : aCompType in self.Components | c.rate > 100 } | P(x)

 

These techniques can be combined as appropriate wherever a SetExpression can be used.  The following example illustrates mixing and matching SetExpressions.

Forall x : int in { select y in { 1, 2, 3, 4, 5 } | y > 2 } | P(x)

 

 

Semantics of select and collect.  The set expression syntax introduces the functions select and collect.  These functions are both set constructors that create a new set from the members of an existing set.[1] The select function acts as a filter that takes a set s and a predicate expression p as arguments and returns a new set s’ that contains the members of the set s that satisfy the predicate p.  The returned set s’ is a subset of the original set s, as the following example illustrates:

{ select v : int in { 1, 2, 3, 4, 5 } | v > 2 } returns the set { 3, 4, 5 }.

 

Like the select function, the collect function acts as a filter on a set s and creates a new set s’ from the elements of s that satisfy the predicate p.  The new set s’, however, is not a subset of the original set s.  Rather, the new set consists of the values of the specified substructure of the original set's elements. The following examples should help to illustrate:

{ collect v.x : int in { [x=4; y=6], [x=5; y=7]; [x=5; y=8] } | v.y – v.x = 2 }
returns the set { 4, 5 }

 

{ collect c.ports : set{port}in self.Components | satisfiesType(c, Filter) }
returns the set { all sets of ports on self’s components that satisfy type Filter }

 

 

Standard sets.  All design elements consist of one or more finite sets that can be dereferenced using the “.” (dot) operator. A list of the standard sets available for various categories of design elements follows.  The basic notation used here is that anything in angle brackets (e.g. <Component> ) refers to a type or category of design element or property.  The item in angle brackets needs to be replaced by a reference to an instance of that category in order to retrieve the desired set.  The standard sets include:

<System>.Components             Refers to the set of components that are instantiated in <System>. Only components whose parent is <System> are returned.  It does not traverse into any representations.

<System>.Connectors Refers to the set of connectors that are instantiated in <System>. Only connectors whose parent is <System> are returned.  It does not traverse into any representations.

<Component>.Ports      Refers to the set of ports defined as interfaces to <Component>.

<Connector>.Roles       Refers to the set of roles defined as interfaces to <Connector>.

<Element>.Representations 
Refers to the set of representations of <Element>

<Element>.Properties   Refers to the set of properties of a design element

<Port>.attachedRoles   Refers to the set of roles that are attached to <Port>.

<Role>.attachedPorts   Refers to the set of ports attached to <Role>.

In addition to these standard sets, the dot notation can be used on elements with set-typed properties to dereference the sets stored in those properties for use in quantification.

 



[1] The select and collect constructs were derived from similar constructs in UML's Object Constraint Language (OCL). Further information on OCL is available at www.omg.org and at www.rational.com/uml/html/ocl.