The KeY Syntax

Abstract

The KeY system accepts different kinds of inputs related to Java Card DL. From the user point of view these inputs can be divided into the following categories:

• system rule files,

• user defined rule files,

• user problem files/proofs with optional user defined rules,

• Java Card DL terms and formulae required by the interaction component of the KeY system.

From the system’s perspective the division is similar, but on top of this, the distinction between schematic mode and term (normal) mode is very important:

• in schematic mode schema variables can be defined and used (usually in definition of rules/taclets) and concrete terms or formulae are forbidden,

• in normal mode schema variables and all other schematic constructs are forbidden, while concrete terms and formulae are allowed.

Additionally, most of terms and formulae constructs can appear in both schematic and normal mode, but take slightly different form depending on the mode.