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

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.

\skolemTerm (SKOLEMTERM)

\applyUpdateOnRigid

\simplifyIfThenElseUpdate

\skolemFormula SKOLEMFORMULA

\termLabel TERMLABEL

\modifies MODIFIES

PROGRAMVARIABLES

SAME_OBSERVER

VARCOND

APPLY_UPDATE_ON_RIGID

DEPENDINGON

DISJOINTMODULONULL

DROP_EFFECTLESS_ELEMENTARIES

DROP_EFFECTLESS_STORES

SIMPLIFY_IF_THEN_ELSE_UPDATE

ENUM_CONST

FREELABELIN

\hasSort (HASSORT)

\fieldType FIELDTYPE

FINAL

ELEMSORT

HASLABEL

HASSUBFORMULAS

ISARRAY

ISARRAYLENGTH

ISCONSTANT

ISENUMTYPE

ISINDUCTVAR

ISLOCALVARIABLE

ISOBSERVER

DIFFERENT

METADISJOINT

ISTHISREFERENCE

DIFFERENTFIELDS

ISREFERENCE

ISREFERENCEARRAY

ISSTATICFIELD

ISSUBTYPE

EQUAL_UNIQUE

NEW

NEW_TYPE_OF

NEW_DEPENDING_ON

HAS_ELEMENTARY_SORT

NEWLABEL

CONTAINS_ASSIGNMENT

NOT_

NOTFREEIN

SAME

STATIC

STATICMETHODREFERENCE

MAXEXPANDMETHOD

STRICT

TYPEOF

INSTANTIATE_GENERIC

SUBST

Term constructs

if-then-else {: #Token-IF} {: #Token-THEN}

A binding if-then-else

File constructs

INCLUDE

INCLUDELDTS

CLASSPATH

BOOTCLASSPATH

NODEFAULTCLASSES

JAVASOURCE

WITHOPTIONS

OPTIONSDECL

KEYSETTINGS

PROFILE

TRUE

FALSE

SAMEUPDATELEVEL

INSEQUENTSTATE

ANTECEDENTPOLARITY

SUCCEDENTPOLARITY

TRIGGER

AVOID

PREDICATES

FUNCTIONS

TRANSFORMERS

UNIQUE

RULES

AXIOMS

PROBLEM

CHOOSECONTRACT

PROOFOBLIGATION

PROOF

PROOFSCRIPT

CONTRACTS

INVARIANTS

LEMMA

IN_TYPE

IS_ABSTRACT_OR_INTERFACE

CONTAINERTYPE

LOCSET

SEQ

BIGINT

UTF_PRECEDES

UTF_IN

UTF_EMPTY

UTF_UNION

UTF_INTERSECT

UTF_SUBSET

UTF_SETMINUS

SEMI

SLASH

COLON

DOUBLECOLON

ASSIGN

DOT

COMMA

LPAREN

RPAREN

LBRACE

RBRACE

LBRACKET

RBRACKET

AT

EQUALS

EXP

TILDE

PERCENT

STAR

MINUS

PLUS

GREATER

LESS

DOC_COMMENT

ML_COMMENT

MODALITYD

MODALITYB

MODALITYBB

MODAILITYGENERIC1

MODAILITYGENERIC2

MODAILITYGENERIC3

MODAILITYGENERIC4

MODAILITYGENERIC5

MODAILITYGENERIC6

MODAILITYGENERIC7

MODALITYD_END

MODALITYG_END

MODALITYB_END

MODALITYBB_END