| TupleTerm |
( t1,...,tn ) where t1,...,tn are terms, that can have a distinct nature. The empty tuple is not allowed. |
| SequenceTerm |
[ t1,...,tn ] where t1,...,tn are terms of the same nature. [ ] denotes the empty sequence. A finite sequence over numbers (real, integer and natural) can be also defined by means of an interval notation, as in [ tlow : tupp [ ,s ] ] where: - tlow and tuppare numbers representing, respectively, the lower and the upper elements of the sequence. - s is a positive number representing the step used to take the elements. If s is omitted it is assumed "s=1" by default. |
| SequenceCT |
[v1 in S1,...,vn in Sn [|Gv1,...,vn ] : tv1,...,vn] where: - v1,...,vn are variables. - tv1,...,vn is the main term containing free occurrences of v1,...,vn. - S1,...,Sn are terms representing the sequences where the variables v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "true" as default condition. |
| SetTerm |
{ t1,...,tn } where t1,...,tn are terms of the same nature. { } denotes the empty set. A finite set over numbers (real, integer and natural) can be also defined by means of an interval notation, as in [ tlow : tupp [ ,s ] ] where: - tlow and tupp are real number representing, respectively, the lower and the upper elements of the set - s is a positive number representing the step used to take the elements. If s is omitted it is assumed "s=1" by default. |
| SetCT |
{v1 in D1,...,vn in Dn [|Gv1,...,vn ] : tv1,...,vn} where: - v1,...,vn are variables. - tv1,...,vn is the main term containing free occurrences of v1,...,vn. - D1,...,Dn are terms representing the domains where the variables v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "true" as default condition. |
| BagTerm |
< t1,...,tn > where t1,...,tn are terms of the same nature. < > denotes the empty bag. The notation for a bag of bags needs at least one space before to list the bag elements as in <<... >,...,<...>>. A finite bag over numbers (real, integer and natural) can be also defined by means of an interval notation, as in [ tlow : tupp [ ,s ] ] where: - tlow and tupp are real number representing, respectively, the lower and the upper elements of the bag. - s is a positivel number representing the step used to take the elements. If s is omitted it is assumed "s=1" by default. |
| BagCT |
< in B1,...,vn in Bn [|Gv1,...,vn ] : tv1,...,vn > where: - v1,...,vn are variables. - tv1,...,vn is a term containing free occurrences of v1,...,vn. - B1,...,Bn are terms representing the bags where the variables v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "true" as default condition. |
| MapTerm |
{t1 -> s1,...,tn -> sn } where: - t1,...,tn are terms of the same nature. - s1,...,sn are terms of the same nature. { ->} denotes the empty map. |
| MapCT |
{v1 in D1,...,vn in Dn [|Gv1,...,vn ] : tv1,...,vn -> sv1,...,vn } where: - v1,...,vn are variables. - tv1,...,vn sv1,...,vnare terms containing free occurrences of v1,...,vn. - D1,...,Dn are terms representing the domains where the variables v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "true" as default condition. |
| ConditionalTerm |
ifG then tthen [else telse ] endif where: - G is a term representing a boolean condition. - tthen and telse are terms of the same nature. If telse is omitted it is assumed "else undef" as default. |
| CaseTerm |
switch t case t1 : s1 ... case tn : sn [ otherwise sn+1 ] endswitch where: - t,t1,...,tn are terms of the same nature. - s1,...,sn,sn+1 are terms of the same nature. If sn+1 is omitted it is assumed "otherwise undef" as default. |
| LetTerm |
let ( v1=t1, ..., vn=tn ) in tv1,...,vn endlet where: - v1,...,vn are variables. - t1,...,tn are terms. - tv1,...,vn is a term containing free occurrences of v1,...,vn. |
| ExistTerm |
( exist v1 in D1,...,vn in Dn[ with Gv1,...,vn ]) where: - v1,...,vn are variables. - D1,...,Dn are terms representing the domains where v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "with true" as default condition. |
| ExistUniqueTerm |
( exist unique v1 in D1,...,vn in Dn[ with Gv1,...,vn ]) where: - v1,...,vn are variables. - D1,...,Dn are terms representing the domains where v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "with true" as default condition. |
| ForallTerm |
( forall v1 in D1,...,vn in Dn[ with Gv1,...,vn ]) where: - v1,...,vn are variables. - D1,...,Dn are terms representing the domains where v1,...,vn take their value. - Gv1,...,vn is a term representing a boolean condition containing occurrences of v1,...,vn. If Gv1,...,vn is omitted it is assumed "with true" as default condition. |
| DomainTerm |
D where D is the name of a domain declared in the ASM signature or directly the expression for a structured type-domain. |
| RuleAsTerm |
<< R[ ( D1,...,Dn ) ] >> where R is the name of a defined transition rule, and D1,...,Dn (if any) are the domains of the formal rule parameters. It is a special term used to denote a transition rule where a term is expected (e.g as actual parameter in a rule application to represent a transition rule). Itsinterpretation results, therefore, in a transition rule. Similarly to functions, rules can be overloaded. When rules are overloaded, it is necessary to indicate the domains of the formal rule parameters. |