|
|
| (One intermediate revision by the same user not shown) |
| Line 1: |
Line 1: |
| − | <noinclude> [[MELD features]] </noinclude>
| + | Do you mean: [[MELD features/Appendix C]] ? |
| − | = Appendix C: BNF Grammar for MELD =
| + | Or the top level page: [[MELD features]] ? |
| − | | |
| − | This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled with the 650 formulas above in Appendix A, -- to check a MELD formula for semantic well-formedness as well.
| |
| − | | |
| − | Assume the following Terminals (token-level non-terminals)
| |
| − | <pre>
| |
| − | <Character>
| |
| − | <String>
| |
| − | <Number>
| |
| − | <Symbol>
| |
| − | <Variable>
| |
| − | | |
| − | Assume the following MELD data object:
| |
| − | | |
| − | <Constant>
| |
| − | | |
| − | The empty expansion is:
| |
| − | | |
| − | <epsilon>
| |
| − | | |
| − | | |
| − | ;;;;;;;;;;;;;;;;;;;;;;;;
| |
| − | ;; Syntactic Constraints
| |
| − | ;;;;;;;;;;;;;;;;;;;;;;;;
| |
| − | | |
| − | <Formula> ::= #$True
| |
| − | | #$False
| |
| − | | <Variable>
| |
| − | | <Literal>
| |
| − | | <NotForm>
| |
| − | | <AndForm>
| |
| − | | <OrForm>
| |
| − | | <XorForm>
| |
| − | | <ImpForm>
| |
| − | | <EquivForm>
| |
| − | | <UnivForm>
| |
| − | | <ExistForm>
| |
| − | | <ExistExactForm>
| |
| − | | <ExistUBoundForm>
| |
| − | | <ExistLBoundForm>
| |
| − | | |
| − | <Formula-Seq> ::= <Formula> <Formula-Seq>
| |
| − | | . <Variable>
| |
| − | | <epsilon>
| |
| − | | |
| − | <NotForm> ::= ( #$not <Formula> )
| |
| − | | |
| − | <AndForm> ::= ( #$and <Formula-Seq> )
| |
| − | | |
| − | <OrForm> ::= ( #$or <Formula-Seq> )
| |
| − | | |
| − | <XorForm> ::= ( #$xor <Formula> <Formula> )
| |
| − | | |
| − | <ImpForm> ::= ( #$implies <Formula> <Formula> )
| |
| − | | |
| − | <EquivForm> ::= ( #$equivalent <Formula> <Formula> )
| |
| − | | |
| − | <UnivForm> ::= ( #$forAll <Variable> <Formula> )
| |
| − | | |
| − | <ExistForm> ::= ( #$thereExists <Variable> <Formula> )
| |
| − | | |
| − | <ExistExactForm> ::= ( #$thereExistExactly <1stOrderTerm> <Variable> <Formula> )
| |
| − | | |
| − | <ExistUBoundForm> ::= ( #$thereExistAtMost <1stOrderTerm> <Variable> <Formula> )
| |
| − | | |
| − | <ExistLBoundForm> ::= ( #$thereExistAtLeast <1stOrderTerm> <Variable> <Formula> )
| |
| − | | |
| − | <Literal> ::= <AtomicFormula>
| |
| − | | ( #$not <AtomicFormula> )
| |
| − |
| |
| − | <AtomicFormula> ::= ( <Predicate> <Argument-Seq> )
| |
| − | | |
| − | <Argument-Seq> ::= <2ndOrderTerm> <Argument-Seq>
| |
| − | | . <Variable>
| |
| − | | <epsilon>
| |
| − | | |
| − | <Predicate> ::= <Rep1stOrderTerm>
| |
| − | | |
| − | <FunctionExp> ::= ( <Function> <Argument-Seq> )
| |
| − | | |
| − | <Function> ::= <Rep1stOrderTerm>
| |
| − | | |
| − | <2ndOrderTerm> ::= <1stOrderTerm>
| |
| − | | <Formula>
| |
| − | | |
| − | <1stOrderTerm> ::= <Rep1stOrderTerm>
| |
| − | | <PrimitiveTerm>
| |
| − | | |
| − | <Rep1stOrderTerm> ::= <Constant>
| |
| − | | <FunctionExp>
| |
| − | | <Variable>
| |
| − | | |
| − | <PrimitiveTerm> ::= <Character>
| |
| − | | <String>
| |
| − | | <Number>
| |
| − | | <Symbol>
| |
| − | | <Variable>
| |
| − | | |
| − | ;;;;;;;;;;;;;;;;;;;;;;;
| |
| − | ;; Semantic Constraints
| |
| − | ;;;;;;;;;;;;;;;;;;;;;;;
| |
| − | | |
| − | For <ExistExactForm> :
| |
| − | | |
| − | 1st arg must denote a positive integer
| |
| − |
| |
| − | For <ExistUBoundForm> :
| |
| − | | |
| − | 1st arg must denote a positive integer
| |
| − |
| |
| − | | |
| − | For <ExistLBoundForm> :
| |
| − | | |
| − | 1st arg must denote a positive integer
| |
| − | | |
| − | For <Function> :
| |
| − | | |
| − | when <Function> is ground
| |
| − | (#$isa <Function> #$NonPredicateFunction) must be true
| |
| − | | |
| − | For <Predicate> :
| |
| − | when <Predicate> is ground
| |
| − | (#$isa <Predicate> #$Predicate) must be true
| |
| − | | |
| − | | |
| − | Relation Arity Constraints:
| |
| − |
| |
| − | For <FunctionExp> :
| |
| − | when <Function> is ground
| |
| − | either
| |
| − | (#$isa <Function> #$VariableArityRelation)
| |
| − | or
| |
| − | (#$arity <Function> <N>)
| |
| − | and
| |
| − | <N> is a non-negative integer
| |
| − | and
| |
| − | if <Argument-Seq> is terminated by . <Variable>
| |
| − | the number of <2ndOrderTerm>s in <Argument-Seq>
| |
| − | must be less than or equal to <N>
| |
| − | else the number of <2ndOrderTerm>s in <Argument-Seq>
| |
| − | must be equal to <N>
| |
| − | | |
| − | For <AtomicFormula> :
| |
| − |
| |
| − | when <Predicate> is ground
| |
| − | either
| |
| − | (#$isa <Predicate> #$VariableArityRelation)
| |
| − |
| |
| − | or
| |
| − | (#$arity <Predicate> <N>)
| |
| − | and
| |
| − | <N> is a non-negative integer
| |
| − | and
| |
| − | if <Argument-Seq> is terminated by . <Variable>
| |
| − | the number of <2ndOrderTerm>s in <Argument-Seq>
| |
| − | must be less than or equal to <N>
| |
| − | else the number of <2ndOrderTerm>s in <Argument-Seq>
| |
| − | must be equal to <N>
| |
| − | | |
| − | Relation Argument Constraints:
| |
| − | | |
| − | For <FunctionExp> :
| |
| − | | |
| − | each term in <Argument-Seq> must satisfy all applicable arg constraints
| |
| − | (e.g., #$arg1Isa, #$interArgIsa2-1, ...)
| |
| − | | |
| − | or <AtomicFormula> :
| |
| − | | |
| − | each term in <Argument-Seq> must satisfy all applicable arg constraints
| |
| − | (e.g., #$arg1Isa, #$interArgIsa2-1, ...)
| |
| − | </pre>
| |
