# Gappa language¶

Comments begin with a sharp sign # and go till the end of the line. Comments beginning by #@ are handled as embedded command-line options. All these comments are no different from a space character.

Space, tabulation, and line-break characters are not significant, they at most act as identifier separators. In the definition part of a script, the GE is never matched, so no separator is needed between operators > and =.

## Tokens and operator priority¶

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})?


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


## Grammar¶

 0 $accept: BLOB$end

1 BLOB: BLOB1 HINTS

2 BLOB1: PROG '{' PROP '}'

3 PROP: REAL LE SNUMBER
4     | FIX '(' REAL ',' SINTEGER ')'
5     | FLT '(' REAL ',' INTEGER ')'
6     | REAL IN '[' SNUMBER ',' SNUMBER ']'
7     | REAL IN '?'
8     | REAL GE SNUMBER
9     | REAL RDIV REAL IN '[' SNUMBER ',' SNUMBER ']'
10     | '|' REAL RDIV REAL '|' LE NUMBER
11     | REAL RDIV REAL IN '?'
12     | REAL '=' REAL
13     | PROP AND PROP
14     | PROP OR PROP
15     | PROP IMPL PROP
16     | NOT PROP
17     | '(' PROP ')'

18 SNUMBER: NUMBER
19        | '+' NUMBER
20        | '-' NUMBER

21 INTEGER: NUMBER

22 SINTEGER: SNUMBER

23 FUNCTION_PARAM: SINTEGER
24               | IDENT

25 FUNCTION_PARAMS_AUX: FUNCTION_PARAM
26                    | FUNCTION_PARAMS_AUX ',' FUNCTION_PARAM

27 FUNCTION_PARAMS: /* empty */
28                | '<' FUNCTION_PARAMS_AUX '>'

29 FUNCTION: FUNID FUNCTION_PARAMS

30 EQUAL: '='
31      | FUNCTION '='

32 PROG: /* empty */
33     | PROG IDENT EQUAL REAL ';'
34     | PROG '@' IDENT '=' FUNCTION ';'
35     | PROG VARID
36     | PROG FUNID
37     | PROG '@' VARID
38     | PROG '@' FUNID

39 REAL: SNUMBER
40     | VARID
41     | IDENT
42     | FUNCTION '(' REALS ')'
43     | REAL '+' REAL
44     | REAL '-' REAL
45     | REAL '*' REAL
46     | REAL '/' REAL
47     | '|' REAL '|'
48     | SQRT '(' REAL ')'
49     | FMA '(' REAL ',' REAL ',' REAL ')'
50     | '(' REAL ')'
51     | '+' REAL
52     | '-' REAL

53 REALS: REAL
54      | REALS ',' REAL

55 DPOINTS: SNUMBER
56        | DPOINTS ',' SNUMBER

57 DVAR: REAL
58     | REAL IN INTEGER
59     | REAL IN '(' DPOINTS ')'

60 DVARS: DVAR
61      | DVARS ',' DVAR

62 PRECOND: REAL NE SINTEGER
63        | REAL LE SINTEGER
64        | REAL GE SINTEGER
65        | REAL '<' SINTEGER
66        | REAL '>' SINTEGER

67 PRECONDS_AUX: PRECOND
68             | PRECONDS_AUX ',' PRECOND

69 PRECONDS: /* empty */
70         | '{' PRECONDS_AUX '}'

71 HINTS: /* empty */
72      | HINTS REAL IMPL REAL PRECONDS ';'
73      | HINTS REALS '$' DVARS ';' 74 | HINTS PROP '$' DVARS ';'
75      | HINTS '\$' DVARS ';'
76      | HINTS REAL '~' REAL ';'


## Logical formulas¶

These sections describe some properties of the logical fragment Gappa manipulates. Notice that this fragment is sound, as the generated formal proofs depend on the support libraries, and these libraries are formally proved by relying only on the axioms of basic arithmetic on real numbers.

### Undecidability¶

First, notice that the equality of two expressions is equivalent to checking that their difference is bounded by zero: e - f in [0,0]. Second, the property that a real number is a natural number can be expressed by the equality between its integer part int<dn>(e) and its absolute value |e|.

Thanks to classical logic, a first-order formula can be written in prenex normal form. Moreover, by skolemizing the formula, existential quantifiers can be removed (although Gappa does not allow the user to type arbitrary functional operators in order to prevent mistyping existing operators, the engine can handle them).

As a consequence, a first-order formula with Peano arithmetic (addition, multiplication, and equality, on natural numbers) can be expressed in Gappa’s formalism. It implies that Gappa’s logical fragment is not decidable.

### Expressiveness¶

Equality between two expressions can be expressed as a bound on their difference: e - f in [0,0]. For inequalities, the difference can be compared to zero: e - f >= 0. The negation of the previous propositions can also be used. Checking the sign of an expression could also be done with bounds; here are two examples: e - |e| in [0,0] and e in [0,1] \/ 1 / e in [0,1]. Logical negations of these formulas can be used to obtain strict inequalities. They can also be defined by discarding only the zero case: not e in [0,0].

Disclaimer: although these properties can be expressed, it does not mean that Gappa is able to handle them efficiently. Yet, if a proposition is proved to be true by Gappa, then it can be considered to be true even if the previous “features” were used in its expression.