# Grammar¶

In KeY, there are multiple formal languages for reading specification and logical constructs.

On the specification we have JML* -- a dialect of the Java Modeling Language -- which comes within the Java files. JML specification are parsed and interpreted into JavaDL expression. JavaDL are represented by the Term class hierarchy. They can be pretty-printed with the LogicPrinter and read by facade of the KeyParser. Also the KeyParser is used to read declarations of logical constructs: i.e. sorts, predicates, functions, taclets, transformers, taclet choices, and problem options and definitions.

In the following we dive into the KeyParser, the term hierarchy and operators hierarchy and the expression and declaration syntax.

Internally, every expression is a tree of Terms, whereas the Term class defines a homomorph Abstract Syntax Tree (AST). Each Term has an operator, which defines its meaning, and a list of sub-terms. The internal representation of term is its prefix form, in which the term is printed as a tree of function application.

This format is not intuitive for humans, hence we defined an syntax that also uses infix and postfix notions.

## Expression Syntax¶

Precedence:

1. Label on functions (term «label»)
2. Parallel (||) updates only
3. Assignment (term := term) updates only
4. Equivalence (<->)
5. Implication (->)
6. Disunction (|)
7. Conjunction (&)
8. Equalities (=, !=), Negation (! term), Quantifier , Modality
9. Comparison (<, <=, >=, >)
10. Arithmetik (+,-)
11. Multiplicaiton (*)
12. Division (/ and Modulo (%)
13. Unary minus (- term)
14. Cast ((sort) term)
15. Bracket suffixes, (term[i], term[1,5], term[*], term[a:=2])
16. Final primitives:
17. Parens (( term ))
18. Location set, Location term
19. Substitution {\subst x; y} f(x)
20. If-then-else and Ifex-then-else (\if (a) TRUE \else b)
21. Abbreviaton (@name)
22. Function names and application (T.(U::a), t.query(), a.b@heap2)
23. Literals

# Definition of Taclets¶

## Variable Conditions¶

Variable conditions are additionally conditions that can be added to taclets with the help of the \varcond(...) construct. Consider the example:

rules {
xyz {
\find(...)

\varcond(\new(#boolv, boolean))

\replacewidth(...)

}
}


Internally, variable conditions correspond the MatchCondition class. With the new parser creating and adding variable conditions will be simplified.

### \sameObserver (SAME_OBSERVER¶

A variable condition that is satisfied if the two arguments are schema variables, their instantiations are terms of observer functions, with the same function, which as exactly one heap argument and has got a dependency contract,

Limitations: Currently, this and de.uka.ilkd.key.rule.metaconstruct.ObserverEqualityMetaConstruct only support observers with a single heap argument, that should be generalised.