There are five composite operators: `/\`

(`AND`

)
and `\/`

(`OR`

) and `->`

(`IMPL`

) and `<=`

(`LE`

) and
`>=`

(`GE`

). And three keywords: `in`

(`IN`

) and `not`

(`NOT`

) and `sqrt`

(`SQRT`

).

Numbers are either written with a binary representation, or with a
decimal representation. In both representations, the `{integer}`

parts are radix-10 natural numbers.

binary {integer}([bB][-+]?{integer})? decimal (({integer}(\.{integer}?)?)|(\.{integer}))([eE][-+]?{integer})? hexadecimal 0x(({hexa}(\.{hexa}?)?)|(\.{hexa}))([pP][-+]?{integer})? number ({binary}|{decimal}|{hexadecimal})

These three expressions represent the same number: `57.5e-1`

,
`23b-2`

, `0x5.Cp0`

. They do not have the same semantic
for Gappa though and a different property will be proved in the decimal case.
Indeed, some decimal numbers cannot be expressed as a dyadic number and Gappa
will have to harden the proof and add a layer to take this into account. In
particular, the user should refrain from being inventive with the constant 1.
For example, writing this constant as `00100.000e-2`

may prevent
some rewriting rules to be applied.

Identifiers (`IDENT`

) are matched by
`{alpha}({alpha}|{digit}|_)*`

.

The associativity and priority of the operators in logical formulas is as follows. It is meant to match the usual conventions.

%right IMPL %left OR %left AND %left NOT

For the mathematical expressions, the priority are as follows. Note that
`NEG`

is the priority of the unary minus; this is the operator with
the highest precedence.

%left '+' '-' %left '*' '/' %left NEG