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>