Syntax of the Assertion Language

 

<assertion>     --> <rule>
                 |  <constraint>

<rule>          --> forall <variableBindList> ( <formula> ) ==> <literal>
                 |  <formula> ==> <literal>
                 |  <literal>

<constraint>    --> <formula>

<formula>       --> exists <variableBindList> <formula>
                 |  forall <variableBindList> <formula>
                 |  not <formula>
                 |  <formula> <==> <formula>
                 |  <formula> ==> <formula>
                 |  <formula> and <formula>
                 |  <formula> or <formula>
                 |  ( <formula> )
                 |  <literal>
                 |  <literal2>

<variableBindList>--> <variableBind> <variableBindList>
                   |  <variableBind>

<variableBind>  --> <varList> / <objectname>
                 |  <varList> / [ <objList> ]
                 |  ALPHANUM / <selectExpB>

<varList>       --> ALPHANUM , <varList>
                 |  ALPHANUM

<objectname>    --> <label>
                 |  <selectExpA>
                 |  <deriveExp>

<label>         --> ALPHANUM
                 |  LABEL
                 |  NUMBER

<literal>       --> FUNCTOR ( <literalArgList> )
                 |  ( <literalArg> <infixSymbol> <literalArg> )
                 |  BOOLEAN

<literal2>      --> ( <label> in <selectExpB> )
                 |  ( <selectExpA> in <selectExpB> )
                 |  ( <selectExpB> isA <selectExpB> )
                 |  ( <selectExpB> = <selectExpB> )

<infixSymbol>   --> INFIXSYMBOL
                 |  <label>

<literalArgList>--> <literalArg> , <literalArgList>
                 |  <literalArg>

<literalArg>    --> <objectname>

<selectExpA>    --> <selectExpA> <selector> <selectExpA>
                 |  ( <selectExpA> )
                 |  <label>

<selector>      --> SELECTOR1
                 |  SELECTOR2

<deriveExp>     --> <label> [ <deriveExpList> ]

<deriveExpList> --> <singleExp> , <deriveExpList>
                 |  <singleExp>

<singleExp>     --> <label> / <label>
                 |  <label> : <label>

<selectExpB>    --> <label> SELECTORB <label>
                 |  <label> SELECTORB <selectExpB2>
                 |  <label> SELECTORB <restriction>

<selectExpB2>   --> <selectExpB>
                 |  <restriction> SELECTORB <label>
                 |  <restriction> SELECTORB <selectExpB2>
                 |  <restriction> SELECTORB <restriction>

<restriction>   --> ( <label> : <label> )
                 |  ( <label> : <selectExpA> )
                 |  ( <label> : <selectExpB> )
                 |  ( <label> : [ <objList> ] )

<objList>       --> <objectname> , <objList>
                 |  <objectname>