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:
- Label on functions (
term «label») - Parallel (
||) updates only - Assignment (
term := term) updates only - Equivalence (
<->) - Implication (
->) - Disunction (
|) - Conjunction (
&) - Equalities (
=,!=), Negation (! term), Quantifier , Modality - Comparison (
<, <=, >=, >) - Arithmetik (
+,-) - Multiplicaiton (
*) - Division (
/and Modulo (%) - Unary minus (
- term) - Cast (
(sort) term) - Bracket suffixes, (
term[i],term[1,5],term[*],term[a:=2]) - Final primitives:
- Parens (
( term )) - Location set, Location term
- Substitution
{\subst x; y} f(x) - If-then-else and Ifex-then-else (
\if (a) TRUE \else b) - Abbreviaton (
@name) - Function names and application (
T.(U::a),t.query(),a.b@heap2) - Literals
Declaration Syntax and Keywords¶
Reference¶
SORTS¶
GENERIC¶
PROXY¶
EXTENDS¶
ONEOF¶
ABSTRACT¶
SCHEMAVARIABLES¶
SCHEMAVAR¶
MODALOPERATOR¶
PROGRAM¶
FORMULA¶
TERM¶
UPDATE¶
VARIABLES¶
VARIABLE¶
HEURISTICSDECL¶
Definition of Taclets¶
General definition¶
Goals¶
CLOSEGOAL¶
REPLACEWITH¶
ADDRULES¶
ADDPROGVARS¶
Attributes¶
NONINTERACTIVE¶
DISPLAYNAME¶
HELPTEXT¶
HEURISTICS¶
FIND¶
ADD¶
ASSUMES¶
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.