Language Constructs¶
Proof scripts are textual representations of rule applications, settings changes and strategy invocations (in the case of KeY as underlying verification system also referred to as macros).
Variables and Types¶
We need to distinguish between: logic, program, and script variables.

logic variable: Occur on sequents, bounded by a quantifier or in an update

program variable: declared and used in Java programs. They are constants on the sequent.

script variable: declared and assignable within a script
Proof Script Language has script variables.
A script variable has a name, a type and a value. Variables are declared by
var0 : type;
var1 : type := value;
var2 := value;
Both statements declare a variable, in the latter case (var1
and var2
) we directly assign a value, in
the first form var0
receives a default value.
Types and Literals¶
We have following types: INT
, TERM<Sort>
, String
.

INT
represents integer of arbitrary size.42 134

TERM<S>
represents a term of sortS
in KeY.S
can be any sort given by KeY. If the sort is ommitied, thenS=Any
.
`f(x)`
`g(a)`
`imp(p,q)`
STRING
"i am a string"
Special Variables¶
To expose settings of the underlying prover to the user we include special variables:
MAX_STEPS
: amount denotes the maximum number of proof steps the underlying prover is allowed to perform
Proof Commands¶
Proof commands start with an identifier followed by optional arguments:
command argName="argument" "positional argument" ;
Every command is terminated with a semicolon. There are named arguments in the
form argName="argument" and unnamed argument without name. Single '...'
and
double quotes "..."
can both be used.
Singleline comments are start with //
.
KeY Rules/Taclets¶
All KeY rules can be used as proof command. The following command structure is used to apply single KeY rules onto the sequent of a selected goal node. If no argument is following the proof command the taclet corresponding to this command has to match at most once on the sequent.
If more terms or formulas to which a proof command is applicable exist, arguments have to be given that indicate the where to apply the rule to.
A rule command has the following syntax:
RULENAME [on=TERM]?
[formula=TERM]
[occ=INT]
[inst_*=TERM]
with:
TERM
specific subtermTOP_LEVEL_FORMULA
: specific top level formulaOCCURENCE_IN_SEQUENT
: Number of occurence in the sequentmaxSteps
the number of steps KEY should at most use until it terminateds teh proof search
If a rule has schema variables which must be instantiated manually, such instantiations can be provided as arguments. A schema variable named sv can be instantiated by setting the argument sv="..." or by setting inst_sv="..." (the latter works also for conflict cases like inst_occ="...").
Examples¶
andRight;
Applicable iff there is only one matching spot on the sequent

eqSymm formula="a=b";
This command changes the sequent
a=b ==> c=d
tob=a ==> c=d
Using onlyeqSymm;
alone would have been ambiguous. 
eqSymm formula="a=b>c=d" occ=2;
This command changes sequent
a=b>c=d ==>
toa=b>d=c ==>
. The occurrence number is needed since there are two possible applications on the formula 
eqSymm formula="a=b>c=d" on="c=d";
This command changes the sequent "a=b>c=d ==>" to "a=b>d=c ==>". It is simialr to the example above, but here the option to specify a subterm instead of an occurrence number is used.

cut cutFormula="x > y";
This command is almost the same as cut \
x>y``
MacroCommands¶
In the KeY system macro commands are proof strategies tailored to specific proof tasks. The available macro commands can be found using the command help. Using them in a script is similar to using rule commands:
MACRONAME (PARAMETERS)?
Often used macro commands are:
 symbex : performs symbolic execution
 auto: invokes the automatic strategy of key
 heap_simp: performs heap simplification
 autopilot: full autopilot
 autopilot_prep: preparation only autopilot
 split_prop: propositional expansion w/ splits
 nosplit_prop: propositional expansion w/o splits
 simp_upd: update simplification
 simp_heap: heap simplification
Example:
auto;
Selectors
As nited before proof commands are implemented as single goal statements.
Some proof commands split a proof into more than one goal.
To allow to apply proof commands in proof state with more than one proof goal, the language allows for
a selector statement cases. Such a casesstatement has the following structure:
cases {
case MATCHER:
STATEMENTS
[default:
STATEMENTS]?
}
Control Flow Statements
The script language allows different statements for controlflow. ControlFlow statements define blocks, therefor it is neccessary to use curly braces after a controlflow statement.
 foreach {STATEMENTS}
 theOnly {STATEMENTS}
 repeat {STATEMENTS}